Documentation

Lean.Meta.Match.Basic

Equations
Instances For
    Instances For
      Equations
      Instances For

        Apply the free variable substitution s to the given pattern

        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Match alternative

            • ref : Syntax

              Syntax object for providing position information

            • idx : Nat

              Original alternative index. Alternatives can be split, this index is the original position of the alternative that generated this one.

            • rhs : Expr

              Right-hand-side of the alternative.

            • fvarDecls : List LocalDecl

              Alternative pattern variables.

            • patterns : List Pattern

              Alternative patterns.

            • cnstrs : List (Expr × Expr)

              Pending constraints lhs ≋ rhs that need to be solved before the alternative is considered acceptable. We generate them when processing inaccessible patterns. Note that lhs and rhs often have different types. After we perform additional case analysis, their types become definitionally equal.

            Instances For
              Equations
              Instances For
                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
                    def Lean.Meta.Match.Alt.replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Return true if fvarId is one of the alternative pattern variables

                      Equations
                      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 _ _ _)), _
                        
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Instances For
                                def Lean.Meta.Match.withGoalOf {α : Type} (p : Problem) (x : MetaM α) :
                                Equations
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Instances For

                                      Convert a expression occurring as the argument of a match motive application back into a Pattern For example, we can use this method to convert x::y::xs at

                                      ...
                                      (motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : (x y : Nat) → (xs : List Nat) → motive (x :: y :: xs))
                                      ...
                                      

                                      into a pattern object

                                      Match congruence equational theorem names helper declarations and functions