def Hect (n : Nat) (A : Vect n (Sort u)) : Sort u

Equations

• Hect n A = ((i : Fin n) → A i)

def Hect.nil {A : Vect 0 (Sort u_1)} : Hect 0 A

def Hect.cons {A : Sort u_1} {n : Nat} {T : Vect n (Sort u_1)} (head : A) (tail : Hect n T) : Hect (n + 1) (A :: T)

Equations

• head ::: tail = Fin.cases head tail

def hect_cons : Lean.TrailingParserDescr

Equations

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