class LeanSubst.PrefixHash (T : Type u) : Type u

• hash : Nat → T

def LeanSubst.«term#_» : Lean.ParserDescr

Equations

• LeanSubst.«term#_» = Lean.ParserDescr.node `LeanSubst.«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

class LeanSubst.PrefixPercent (T : Type u) (F : Type u → Type u) : Type u

• percent : T → F T

def LeanSubst.«term%_» : Lean.ParserDescr

Equations

• LeanSubst.«term%_» = Lean.ParserDescr.node `LeanSubst.«term%_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") (Lean.ParserDescr.cat `term 1024))