Documentation

Lean.HeadIndex

inductive Lean.HeadIndex :

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.

Instances For

    Hash code for a HeadIndex value.

    Equations
    Instances For

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

      Equations
      Instances For

        Convert the given expression into a HeadIndex.

        Equations
        Instances For