inductive Lilac.Vec (α : Sort u) : Nat → Sort (max u 1)

• nil {α : Sort u} : Vec α 0
• cons {α : Sort u} {n : Nat} : α → Vec α n → Vec α (n + 1)

def Lilac.«term#()» : Lean.ParserDescr

Equations

• Lilac.«term#()» = Lean.ParserDescr.node `Lilac.«term#()» 1024 (Lean.ParserDescr.symbol "#()")

def Lilac.vec_cons : Lean.TrailingParserDescr

Equations

• Lilac.vec_cons = Lean.ParserDescr.trailingNode `Lilac.vec_cons 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

def Lilac.Vec.repr {α : Type u_1} {n : Nat} [Repr α] (v : Vec α n) (p : Nat) : Std.Format

Equations

• v.repr p = Std.Format.text "#(" ++ Lilac.Vec.repr.go v p ++ Std.Format.text ")"

def Lilac.Vec.repr.go {α : Type u_1} {n : Nat} [Repr α] : Vec α n → Nat → Std.Format

Equations

• Lilac.Vec.repr.go #() x✝ = Std.Format.text ""
• Lilac.Vec.repr.go (x_2 :: #()) x✝ = repr x_2
• Lilac.Vec.repr.go (x_2 :: xs) x✝ = repr x_2 ++ Std.Format.text "," ++ Lilac.Vec.repr.go xs x✝

@[implicit_reducible]

instance Lilac.instReprVec {n : Nat} {α : Type u} [Repr α] : Repr (Vec α n)

Equations

• Lilac.instReprVec = { reprPrec := Lilac.Vec.repr }

def Lilac.«term#(_,)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lilac.Vec.unexpand_nil : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Lilac.Vec.unexpand_cons : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Lilac.Fun.Vec.to {α : Sort u_1} {n : Nat} (v : Vec α n) : Lilac.Vec α n

Equations

• ↑v = Lilac.Fun.Vec.induction #() (fun {n : Nat} (hd : α) (x : Lilac.Fun.Vec α n) (tl : Lilac.Vec α n) => hd :: tl) v

@[implicit_reducible]

instance Lilac.instCoeVecVec {α : Sort u_1} {n : Nat} : Coe (Fun.Vec α n) (Vec α n)

Equations

• Lilac.instCoeVecVec = { coe := Lilac.Fun.Vec.to }

def Lilac.Vec.to {α : Sort u_1} {n : Nat} : Vec α n → Fun.Vec α n

Equations

• #().to = Lilac.Fun.Vec.nil
• (x_1 :: xs).to = Lilac.Fun.Vec.cons x_1 xs.to

def Lilac.Vec.list {α : Type u_1} {n : Nat} : Vec α n → List α

Equations

• #().list = []
• (x_1 :: xs).list = x_1 :: xs.list

def Lilac.Vec.has_dec_eq {α : Sort u_1} {n : Nat} [DecidableEq α] (a b : Vec α n) : Decidable (a = b)

Equations

• Lilac.Vec.has_dec_eq = sorry

@[implicit_reducible]

instance Lilac.instDecidableEqVec {α : Sort u_1} {n : Nat} [DecidableEq α] : DecidableEq (Vec α n)

Equations

• Lilac.instDecidableEqVec = Lilac.Vec.has_dec_eq

@[reducible]

def Lilac.Vec.length {α : Sort u_1} {n : Nat} : Vec α n → Nat

Equations

• x✝.length = n

def Lilac.Vec.head {α : Sort u_1} {n : Nat} [NeZero n] : Vec α n → α

Equations

• #().head = ⋯.elim
• (x_4 :: a).head = x_4

def Lilac.Vec.tail {α : Sort u_1} {n : Nat} [NeZero n] : Vec α n → Vec α (n - 1)

Equations

• #().tail = ⋯.elim
• (x_4 :: a).tail = a

def Lilac.Vec.get {α : Sort u_1} {n : Nat} : Vec α n → Fin n → α

Equations

• (x_2 :: xs).get i = Fin.cases x_2 xs.get i

@[implicit_reducible]

instance Lilac.instGetElemVecFinTrue {α : Type u_1} {n : Nat} : GetElem (Vec α n) (Fin n) α fun (x : Vec α n) (x_1 : Fin n) => True

Equations

• Lilac.instGetElemVecFinTrue = { getElem := fun (xs : Lilac.Vec α n) (i : Fin n) (x : True) => xs.get i }

def Lilac.Vec.set {α : Sort u_1} {n : Nat} : Vec α n → Fin n → α → Vec α n

Equations

• (x_3 :: xs).set i x✝ = Fin.cases (x✝ :: xs) (fun (i : Fin n_2) => x_3 :: xs.set i x✝) i

def Lilac.Vec.foldl {α : Type u} {β : Type v} {n : Nat} (f : α → β → α) (init : α) : Vec β n → α

Equations

• Lilac.Vec.foldl f init #() = init
• Lilac.Vec.foldl f init (x_1 :: xs) = Lilac.Vec.foldl f (f init x_1) xs

def Lilac.Vec.foldr {α : Type u} {β : Type v} {n : Nat} (f : α → β → β) (init : β) : Vec α n → β

Equations

• Lilac.Vec.foldr f init #() = init
• Lilac.Vec.foldr f init (x_1 :: xs) = f x_1 (Lilac.Vec.foldr f init xs)

def Lilac.Vec.concat {α : Sort u_1} {n : Nat} : Vec α n → α → Vec α (n + 1)

Equations

• #().concat x✝ = x✝ :: #()
• (x_2 :: xs).concat x✝ = x_2 :: xs.concat x✝

def Lilac.Vec.append {α : Sort u_1} {n m : Nat} : Vec α n → Vec α m → Vec α (m + n)

We intentionally flip the addition order to avoid casting and obtain better simplification

Equations

• #().append x✝ = x✝
• (x_2 :: xs).append x✝ = x_2 :: xs.append x✝

@[implicit_reducible]

instance Lilac.instHAppendVecHAddNat {α : Type u} {n m : Nat} : HAppend (Vec α n) (Vec α m) (Vec α (m + n))

Equations

• Lilac.instHAppendVecHAddNat = { hAppend := Lilac.Vec.append }

def Lilac.Vec.flatten {α : Type u_1} {n m : Nat} : Vec (Vec α n) m → Vec α (n * m)

Equations

• #().flatten = #()
• (x_1 :: xs).flatten = cast ⋯ (x_1 ++ xs.flatten)

def Lilac.Vec.map {α : Type u} {β : Type b} {n : Nat} (f : α → β) : Vec α n → Vec β n

Equations

• Lilac.Vec.map f #() = #()
• Lilac.Vec.map f (x_1 :: xs) = f x_1 :: Lilac.Vec.map f xs

@[implicit_reducible]

instance Lilac.instFunctorVec {n : Nat} : Functor fun (α : Type u_1) => Vec α n

Equations

• Lilac.instFunctorVec = { map := fun {α β : Type ?u.17} => Lilac.Vec.map }

def Lilac.Vec.beq {α : Type u_1} {n m : Nat} [BEq α] : Vec α n → Vec α m → Bool

Equations

• #().beq #() = true
• (x_2 :: xs).beq (y :: ys) = (x_2 == y && xs.beq ys)
• x✝¹.beq x✝ = false

@[implicit_reducible]

instance Lilac.instBEqVec {α : Type u_1} {n : Nat} [BEq α] : BEq (Vec α n)

Equations

• Lilac.instBEqVec = { beq := Lilac.Vec.beq }

def Lilac.Vec.replicate {α : Sort u_1} (n : Nat) (a : α) : Vec α n

Equations

• Lilac.Vec.replicate 0 x✝ = #()
• Lilac.Vec.replicate n.succ x✝ = x✝ :: Lilac.Vec.replicate n x✝

@[reducible]

instance Lilac.instInhabitedVecOfNatNat {α : Sort u_1} : Inhabited (Vec α 0)

Equations

• Lilac.instInhabitedVecOfNatNat = { default := #() }

@[reducible]

instance Lilac.instInhabitedVec {α : Sort u_1} {n : Nat} [Inhabited α] : Inhabited (Vec α n)

Equations

• Lilac.instInhabitedVec = { default := Lilac.Vec.replicate n default }

def Lilac.Vec.reverse {α : Sort u_1} {n : Nat} : Vec α n → Vec α n

Equations

• #().reverse = #()
• (x_1 :: xs).reverse = xs.reverse.concat x_1

def Lilac.Vec.contains {α : Type u_1} {n : Nat} [BEq α] (a : α) : Vec α n → Bool

Equations

• Lilac.Vec.contains a #() = false
• Lilac.Vec.contains a (x_1 :: xs) = (x_1 == a || Lilac.Vec.contains a xs)

def Lilac.Vec.take {α : Sort u_1} {m : Nat} (n : Nat) (h : n ≤ m) : Vec α m → Vec α n

Equations

• Lilac.Vec.take x✝¹ x✝ #() = cast ⋯ #()
• Lilac.Vec.take 0 h x✝ = #()
• Lilac.Vec.take n.succ h (x_3 :: xs) = x_3 :: Lilac.Vec.take n ⋯ xs

def Lilac.Vec.drop {α : Sort u_1} {m : Nat} (n : Nat) (h : n ≤ m) : Vec α m → Vec α (m - n)

Equations

• Lilac.Vec.drop x✝¹ x✝ #() = cast ⋯ #()
• Lilac.Vec.drop 0 h x✝ = x✝
• Lilac.Vec.drop n.succ h (x_3 :: xs) = cast ⋯ (Lilac.Vec.drop n ⋯ xs)

def Lilac.Vec.any {α : Sort u_1} {n : Nat} : Vec α n → (p : α → Bool) → Bool

Equations

• #().any x✝ = false
• (x_2 :: xs).any x✝ = (x✝ x_2 || xs.any x✝)

def Lilac.Vec.all {α : Sort u_1} {n : Nat} : Vec α n → (p : α → Bool) → Bool

Equations

• #().all x✝ = true
• (x_2 :: xs).all x✝ = (x✝ x_2 && xs.any x✝)

def Lilac.Vec.zipWith {α : Type u} {β : Type v} {γ : Type w} {n : Nat} (f : α → β → γ) : Vec α n → Vec β n → Vec γ n

Equations

• Lilac.Vec.zipWith f #() #() = #()
• Lilac.Vec.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: Lilac.Vec.zipWith f xs ys

def Lilac.Vec.zip {α : Type u} {β : Type v} {n : Nat} (v1 : Vec α n) (v2 : Vec β n) : Vec (α × β) n

Equations

• v1.zip v2 = Lilac.Vec.zipWith (fun (x1 : α) (x2 : β) => (x1, x2)) v1 v2

def Lilac.Vec.unzip {α : Type u} {β : Type v} {n : Nat} : Vec (α × β) n → Vec α n × Vec β n

Equations

• #().unzip = (#(), #())
• ((a, b) :: xs).unzip = match xs.unzip with | (as, bs) => (a :: as, b :: bs)

def Lilac.Vec.range (n : Nat) (k : Nat := 0) : Vec Nat n

Equations

• Lilac.Vec.range 0 x✝ = #()
• Lilac.Vec.range n.succ x✝ = x✝ :: Lilac.Vec.range n (x✝ + 1)

def Lilac.Vec.zipIdx {α : Type u_1} {n : Nat} : Vec α n → (k : optParam Nat 0) → Vec (α × Nat) n

Equations

• #().zipIdx x✝ = #()
• (x_2 :: xs).zipIdx x✝ = (x_2, x✝) :: xs.zipIdx (x✝ + 1)

def Lilac.Vec.find? {α : Type u_1} {n : Nat} (p : α → Bool) : Vec α n → Option α

Equations

• Lilac.Vec.find? p #() = none
• Lilac.Vec.find? p (x_1 :: xs) = if p x_1 = true then some x_1 else Lilac.Vec.find? p xs

def Lilac.Vec.findIdx? {α : Sort u_1} {n : Nat} (p : α → Bool) : Vec α n → Option (Fin n)

Equations

• Lilac.Vec.findIdx? p #() = none
• Lilac.Vec.findIdx? p (x_1 :: xs) = Lilac.Vec.findIdx?.go p (x_1 :: xs) 0

def Lilac.Vec.findIdx?.go {α : Sort u_1} (p : α → Bool) {n : Nat} : Vec α n → Nat → Option (Fin n)

Equations

• Lilac.Vec.findIdx?.go p #() x✝ = none
• Lilac.Vec.findIdx?.go p (x_3 :: xs) x✝ = if p x_3 = true then some (Fin.ofNat (n + 1) x✝) else Fin.castSucc <$> Lilac.Vec.findIdx?.go p xs (x✝ + 1)

def Lilac.Vec.erase {α : Type u_1} [BEq α] {n : Nat} : Vec α n → α → (m : Nat) × Vec α m ×' n ≤ m + 1

Equations

• #().erase x✝ = ⟨0, ⟨#(), Lilac.Vec.erase._proof_7⟩⟩
• (x_3 :: xs).erase x✝ = match x_3 == x✝ with | true => ⟨n, ⟨xs, ⋯⟩⟩ | false => match xs.erase x✝ with | ⟨m, ⟨xs', h⟩⟩ => ⟨m + 1, ⟨x_3 :: xs', ⋯⟩⟩

def Lilac.Vec.count {α : Type u_1} {n : Nat} [BEq α] (a : α) : Vec α n → Nat

Equations

• Lilac.Vec.count a #() = 0
• Lilac.Vec.count a (x_1 :: xs) = Lilac.Vec.count a xs + if (x_1 == a) = true then 1 else 0

def Lilac.Vec.traverse {m : Type u_1 → Type u_2} {α : Sort u_3} {β : Type u_1} {n : Nat} [Applicative m] (f : α → m β) : Vec α n → m (Vec β n)

Equations

• Lilac.Vec.traverse f #() = pure #()
• Lilac.Vec.traverse f (x_1 :: xs) = Lilac.Vec.cons <$> f x_1 <*> Lilac.Vec.traverse f xs

def Lilac.Vec.sequence {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Applicative m] : Vec (m α) n → m (Vec α n)

Equations

• Lilac.Vec.sequence = Lilac.Vec.traverse id

def Lilac.Vec.sum {n : Nat} : Vec Nat n → Nat

Equations

• #().sum = 0
• (x_1 :: xs).sum = xs.sum + x_1

inductive Lilac.Vec.Mem {α : Sort u_1} (x : α) {n : Nat} : Vec α n → Prop

• head {α : Sort u_1} {x : α} {x✝ : Nat} {xs : Vec α x✝} : Mem x (x :: xs)
• tail {α : Sort u_1} {x : α} {x✝ : Nat} (y : α) {xs : Vec α x✝} : Mem x xs → Mem x (y :: xs)

@[implicit_reducible]

instance Lilac.instMembershipVec {α : Type u_1} {n : Nat} : Membership α (Vec α n)

Equations

• Lilac.instMembershipVec = { mem := fun (v : Lilac.Vec α n) (x : α) => Lilac.Vec.Mem x v }