def Hequ (A : Sequ (Sort u)) : Sort u

Equations

• Hequ A = ((i : Nat) → A i)

def Hequ.cons {A : Sort u_1} {T : Sequ (Sort u_1)} (head : A) (tail : Hequ T) : Hequ (A :: T)

Equations

• (head ::: tail) 0 = head
• (head ::: tail) n.succ = tail n

def hequ_cons : Lean.TrailingParserDescr

Equations

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