Instances For
- inaccessible: Lean.Expr → Lean.Meta.Match.Pattern
- var: Lean.FVarId → Lean.Meta.Match.Pattern
- ctor: Lake.Name → List Lean.Level → List Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
- val: Lean.Expr → Lean.Meta.Match.Pattern
- arrayLit: Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
- as: Lean.FVarId → Lean.Meta.Match.Pattern → Lean.FVarId → Lean.Meta.Match.Pattern
Instances For
Instances For
Apply the free variable substitution s to the given pattern
Instances For
- ref : Lean.Syntax
- fvarDecls : List Lean.LocalDecl
- patterns : List Lean.Meta.Match.Pattern
Instances For
Instances For
Instances For
- ref : Lean.Syntax
Syntaxobject for providing position information - idx : Nat
Orginal alternative index. Alternatives can be split, this index is the original position of the alternative that generated this one.
- rhs : Lean.Expr
Right-hand-side of the alternative.
- fvarDecls : List Lean.LocalDecl
Alternative pattern variables.
- patterns : List Lean.Meta.Match.Pattern
Alternative patterns.
Match alternative
Instances For
Instances For
Instances For
Instances For
Return true if fvarId is one of the alternative pattern variables
Instances For
Similar to checkAndReplaceFVarId, but ensures type of v is definitionally equal to type of fvarId.
This extra check is necessary when performing dependent elimination and inaccessible terms have been used.
For example, consider the following code fragment:
inductive Vec (α : Type u) : Nat → Type u where
| nil : Vec α 0
| cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop where
| nil : VecPred P Vec.nil
| cons {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
| _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
Recall that _ in a pattern can be elaborated into pattern variable or an inaccessible term.
The elaborator uses an inaccessible term when typing constraints restrict its value.
Thus, in the example above, the _ at Vec.cons head _ becomes the inaccessible pattern .(Vec.nil)
because the type ascription (w : VecPred P Vec.nil) propagates typing constraints that restrict its value to be Vec.nil.
After elaboration the alternative becomes:
| .(0), @Vec.cons .(α) .(0) head .(Vec.nil), @VecPred.cons .(α) .(P) .(0) .(head) .(Vec.nil) h w => ⟨head, h⟩
where
(head : α), (h: P head), (w : VecPred P Vec.nil)
Then, when we process this alternative in this module, the following check will detect that
w has type VecPred P Vec.nil, when it is supposed to have type VecPred P tail.
Note that if we had written
theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
| _, Vec.cons head Vec.nil, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
we would get the easier to digest error message
missing cases:
_, (Vec.cons _ _ (Vec.cons _ _ _)), _
Instances For
- var: Lean.FVarId → Lean.Meta.Match.Example
- underscore: Lean.Meta.Match.Example
- ctor: Lake.Name → List Lean.Meta.Match.Example → Lean.Meta.Match.Example
- val: Lean.Expr → Lean.Meta.Match.Example
- arrayLit: List Lean.Meta.Match.Example → Lean.Meta.Match.Example
Instances For
Instances For
- mvarId : Lean.MVarId
- alts : List Lean.Meta.Match.Alt
- examples : List Lean.Meta.Match.Example
Instances For
Instances For
Instances For
Instances For
Instances For
- matcher : Lean.Expr
- counterExamples : List Lean.Meta.Match.CounterExample
- addMatcher : Lean.MetaM Unit