Documentation

Lean.HeadIndex

inductive Lean.HeadIndex:

Type

instance Lean.instInhabitedHeadIndex:

Inhabited Lean.HeadIndex

Equations

Lean.instInhabitedHeadIndex = { default := Lean.HeadIndex.fvar default }

instance Lean.instBEqHeadIndex:

BEq Lean.HeadIndex

Equations

Lean.instBEqHeadIndex = { beq := [anonymous] }

instance Lean.instReprHeadIndex:

Repr Lean.HeadIndex

Equations

Lean.instReprHeadIndex = { reprPrec := [anonymous] }

def Lean.HeadIndex.HeadIndex.hash:

Lean.HeadIndex → UInt64

Equations

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

instance Lean.HeadIndex.instHashableHeadIndex:

Hashable Lean.HeadIndex

Equations

Lean.HeadIndex.instHashableHeadIndex = { hash := Lean.HeadIndex.HeadIndex.hash }

def Lean.Expr.head:

Lean.Expr → Lean.Expr

def Lean.Expr.headNumArgs (e : Lean.Expr) :

Equations

Lean.Expr.headNumArgs e = Lean.Expr.headNumArgsAux e 0

def Lean.Expr.toHeadIndex (e : Lean.Expr) :

Equations

Lean.Expr.toHeadIndex e = match Lean.Expr.toHeadIndexQuick? e with | some i => i | none => Lean.Expr.toHeadIndexSlow e