- used : Std.HashSet Nat
- counterExamples : List (List Lean.Meta.Match.Example)
Instances For
Note that we decided to store pending constraints to address issues exposed by #1279 and #1361.
Here is a simplified version of the example on this issue (see test: 1279_simplified.lean
)
inductive Arrow : Type → Type → Type 1
| id : Arrow a a
| unit : Arrow Unit Unit
| comp : Arrow β γ → Arrow α β → Arrow α γ
deriving Repr
def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ :=
match f, g with
| id, g => g
| f, id => f
| f, g => comp f g
The initial state for the match
-expression above is
[Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
alternatives:
[β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g
[γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f
[β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g
The first step is a variable-transition which replaces β
with β✝
in the first and third alternatives.
The constraint β✝ ≋ α
in the second alternative used to be discarded. We now store it at the
alternative cnstrs
field.
Given alt
s.t. the next pattern is an inaccessible pattern e
,
try to normalize e
into a constructor application.
If it is not a constructor, throw an error.
Otherwise, if it is a constructor application of ctorName
,
update the next patterns with the fields of the constructor.
Otherwise, return none.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to mkAuxDefinition
, but uses the cache matcherExt
.
It also returns an Boolean that indicates whether a new matcher function was added to the environment or not.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- matcherName : Lean.Name
- matchType : Lean.Expr
- discrInfos : Array Lean.Meta.Match.DiscrInfo
- lhss : List Lean.Meta.Match.AltLHS
Instances For
Equations
- m.numDiscrs = m.discrInfos.size
Instances For
Equations
- m.collectFVars = do m.matchType.collectFVars m.lhss.forM fun (alt : Lean.Meta.Match.AltLHS) => alt.collectFVars
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary method used at mkMatcher
. It executes k
in a local context that contains only
the local declarations m
depends on. This is important because otherwise dependent elimination
may "refine" the types of unnecessary declarations and accidentally introduce unnecessary dependencies
in the auto-generated auxiliary declaration. Note that this is not just an optimization because the
unnecessary dependencies may prevent the termination checker from succeeding. For an example,
see issue #1237.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Create a dependent matcher for matchType
where matchType
is of the form
(a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n]
where n = numDiscrs
, and the lhss
are the left-hand-sides of the match
-expression alternatives.
Each AltLHS
has a list of local declarations and a list of patterns.
The number of patterns must be the same in each AltLHS
.
The generated matcher has the structure described at MatcherInfo
. The motive argument is of the form
(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)
where v
is a universe parameter or 0 if B[a_1, ..., a_n]
is a proposition.
If exceptionIfContainsSorry := true
, then mkMatcher
throws an exception if the auxiliary
declarations contains a sorry
. We use this argument to workaround a bug at IndPredBelow.mkBelowMatcher
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
This function is only used for testing purposes
Equations
- One or more equations did not get rendered due to their size.