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: Lean.FVarId → Lean.HeadIndex
- mvar: Lean.MVarId → Lean.HeadIndex
- const: Lake.Name → Lean.HeadIndex
- proj: Lake.Name → Nat → Lean.HeadIndex
- lit: Lean.Literal → Lean.HeadIndex
- sort: Lean.HeadIndex
- lam: Lean.HeadIndex
- forallE: Lean.HeadIndex
Instances For
Equations
- Lean.instInhabitedHeadIndex = { default := Lean.HeadIndex.fvar default }
Equations
- Lean.instBEqHeadIndex = { beq := Lean.beqHeadIndex✝ }
Equations
- Lean.instReprHeadIndex = { reprPrec := Lean.reprHeadIndex✝ }
Hash code for a HeadIndex
value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.instHashableHeadIndex = { hash := Lean.HeadIndex.hash }
Return the number of arguments in the given expression with respect to its HeadIndex
Equations
- e.headNumArgs = Lean.Expr.headNumArgs.go e 0
Instances For
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
Instances For
Convert the given expression into a HeadIndex
.
Equations
- e.toHeadIndex = match Lean.Expr.toHeadIndexQuick? e with | some i => i | none => Lean.Expr.toHeadIndexSlow e