source
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

Instances For

source
instance Lean.instInhabitedHeadIndex :
Inhabited HeadIndex
Equations

- Lean.instInhabitedHeadIndex = { default := Lean.instInhabitedHeadIndex.default }

source
def Lean.instInhabitedHeadIndex.default :
HeadIndex
Equations

- Lean.instInhabitedHeadIndex.default = Lean.HeadIndex.fvar default

Instances For

source
instance Lean.instBEqHeadIndex :
BEq HeadIndex
Equations

- Lean.instBEqHeadIndex = { beq := Lean.instBEqHeadIndex.beq }

source
def Lean.instBEqHeadIndex.beq :
HeadIndex → HeadIndex → Bool
Equations

- Lean.instBEqHeadIndex.beq (Lean.HeadIndex.fvar a) (Lean.HeadIndex.fvar b) = (a == b)
- Lean.instBEqHeadIndex.beq (Lean.HeadIndex.mvar a) (Lean.HeadIndex.mvar b) = (a == b)
- Lean.instBEqHeadIndex.beq (Lean.HeadIndex.const a) (Lean.HeadIndex.const b) = (a == b)
- Lean.instBEqHeadIndex.beq (Lean.HeadIndex.proj a a_1) (Lean.HeadIndex.proj b b_1) = (a == b && a_1 == b_1)
- Lean.instBEqHeadIndex.beq (Lean.HeadIndex.lit a) (Lean.HeadIndex.lit b) = (a == b)
- Lean.instBEqHeadIndex.beq Lean.HeadIndex.sort Lean.HeadIndex.sort = true
- Lean.instBEqHeadIndex.beq Lean.HeadIndex.lam Lean.HeadIndex.lam = true
- Lean.instBEqHeadIndex.beq Lean.HeadIndex.forallE Lean.HeadIndex.forallE = true
- Lean.instBEqHeadIndex.beq x✝¹ x✝ = false

Instances For

source
def Lean.instReprHeadIndex.repr :
HeadIndex → Nat → Format
Equations

- One or more equations did not get rendered due to their size.
- Lean.instReprHeadIndex.repr Lean.HeadIndex.sort prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.HeadIndex.sort")).group prec✝
- Lean.instReprHeadIndex.repr Lean.HeadIndex.lam prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.HeadIndex.lam")).group prec✝
- Lean.instReprHeadIndex.repr Lean.HeadIndex.forallE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.HeadIndex.forallE")).group prec✝

Instances For

source
instance Lean.instReprHeadIndex :
Repr HeadIndex
Equations

- Lean.instReprHeadIndex = { reprPrec := Lean.instReprHeadIndex.repr }

source
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

Instances For

source
instance Lean.instHashableHeadIndex :
Hashable HeadIndex
Equations

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

source
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

Instances For

source
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

Instances For