Documentation

Lean.HeadIndex

inductive Lean.HeadIndex :

Type

instance Lean.instBEqHeadIndex :

BEq Lean.HeadIndex

Equations

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

instance Lean.instInhabitedHeadIndex :

Inhabited Lean.HeadIndex

Equations

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

def Lean.HeadIndex.HeadIndex.hash :

Lean.HeadIndex → UInt64

Equations

Lean.HeadIndex.HeadIndex.hash x = match x with | Lean.HeadIndex.fvar fvarId => mixHash 11 (hash fvarId) | Lean.HeadIndex.mvar mvarId => mixHash 13 (hash mvarId) | Lean.HeadIndex.const constName => mixHash 17 (hash constName) | Lean.HeadIndex.proj structName idx => mixHash 19 (mixHash (hash structName) (hash idx)) | Lean.HeadIndex.lit litVal => mixHash 23 (hash litVal) | Lean.HeadIndex.sort => 29 | Lean.HeadIndex.lam => 31 | Lean.HeadIndex.forallE => 37

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