inductive Lean.HeadIndex : Type

Datastructure for representing the "head symbol" of an expression. It is the key of KExprMap. Examples:

• The head of f a is .const f
• The head of let x := 1; f x is .const f
• The head of fun x => fun is .lam

HeadIndex is a very simple index, and is used in situations where we want to find definitionally equal terms, but we want to minimize the search by checking only pairs of terms that have the same HeadIndex.

• fvar (fvarId : FVarId) : HeadIndex
• mvar (mvarId : MVarId) : HeadIndex
• const (constName : Name) : HeadIndex
• proj (structName : Name) (idx : Nat) : HeadIndex
• lit (litVal : Literal) : HeadIndex
• sort : HeadIndex
• lam : HeadIndex
• forallE : HeadIndex

instance Lean.instInhabitedHeadIndex : Inhabited HeadIndex

Equations

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

instance Lean.instBEqHeadIndex : BEq HeadIndex

Equations

• Lean.instBEqHeadIndex = { beq := Lean.beqHeadIndex✝ }

instance Lean.instReprHeadIndex : Repr HeadIndex

Equations

• Lean.instReprHeadIndex = { reprPrec := Lean.reprHeadIndex✝ }

def Lean.HeadIndex.hash : HeadIndex → UInt64

Hash code for a HeadIndex value.

Equations

• (Lean.HeadIndex.fvar a).hash = mixHash 11 (hash a)
• (Lean.HeadIndex.mvar a).hash = mixHash 13 (hash a)
• (Lean.HeadIndex.const a).hash = mixHash 17 (hash a)
• (Lean.HeadIndex.proj a a_1).hash = mixHash 19 (mixHash (hash a) (hash a_1))
• (Lean.HeadIndex.lit a).hash = mixHash 23 (hash a)
• Lean.HeadIndex.sort.hash = 29
• Lean.HeadIndex.lam.hash = 31
• Lean.HeadIndex.forallE.hash = 37

instance Lean.instHashableHeadIndex : Hashable HeadIndex

Equations

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

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

Return the number of arguments in the given expression with respect to its HeadIndex

Equations

• e.headNumArgs = Lean.Expr.headNumArgs.go e 0

def Lean.Expr.headNumArgs.go : Expr → Nat → Nat

Equations

• Lean.Expr.headNumArgs.go (f.app arg) x✝ = Lean.Expr.headNumArgs.go f (x✝ + 1)
• Lean.Expr.headNumArgs.go (Lean.Expr.letE declName type value b nonDep) x✝ = Lean.Expr.headNumArgs.go b x✝
• Lean.Expr.headNumArgs.go (Lean.Expr.mdata data e) x✝ = Lean.Expr.headNumArgs.go e x✝
• Lean.Expr.headNumArgs.go x✝¹ x✝ = x✝

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

Convert the given expression into a HeadIndex.

Equations

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