- innerType : Lean.Expr
Collection of variables used to keep track of the positions of binders in the construction
of below
motives and constructors.
Instances For
- params : Array Lean.FVarId
- motives : Array Lean.FVarId
- indices : Array Lean.FVarId
- witness : Lean.FVarId
- indHyps : Array Lean.FVarId
Collection of variables used to keep track of the local context used in the brecOn
proof.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Given a constructor name, find the indices of the corresponding below
version thereof.
Instances For
This function adds an additional below
discriminant to a matcher application.
It is used for modifying the patterns, such that the structural recursion can use the new
below
predicate instead of the original one and thus be used prove structural recursion.
It takes as parameters:
- matcherApp: a matcher application
- belowMotive: the motive, that the
below
type should carry - below: an expression from the local context that is the
below
version of a predicate and can be used for structural recursion - idx: the index of the original predicate discriminant.
It returns:
- A matcher application as an expression
- A side-effect for adding the matcher to the environment
Instances For
Instances For
this function changes the type of the pattern from the original type to the below
version thereof.
Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't
simply recursively change all occurrences, but rather, we recursively change occurences of the constructor.
As such there are only a few cases:
- the pattern is a constructor from the original type. Here we need to:
- replace the constructor
- copy original recursive patterns and convert them to below and reintroduce them in the correct position
- turn original recursive patterns inaccessible
- introduce free variables as needed.
- it is an
as
pattern. Here the contstructor could be hidden inside of it. - it is a variable. Here you we need to introduce a fresh variable of a different type.