Documentation

Lean.Meta.Tactic.ElimInfo

  • name : Name
  • declName? : Option Name

    A declaration corresponding to the inductive constructor. (For custom recursors, the alternatives correspond to parameter names in the recursor, so we may not have a declaration to point to.) This is used for go-to-definition on the alternative name.

  • numFields : Nat
  • provesMotive : Bool

    If provesMotive := true, then this alternative has motive as its conclusion. Only for those alternatives the induction tactic should introduce reverted hypotheses.

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

        Information about an eliminator as used by induction or cases.

        Created from an expression by getElimInfo. This typically contains level metavariables that are instantiated as we go (e.g. in addImplicitTargets), so this is single use.

        • elimExpr : Expr
        • elimType : Expr
        • motivePos : Nat
        • targetsPos : Array Nat
        • altsInfo : Array ElimAltInfo
        • numComplexMotiveArgs : Nat

          Extra arguments to the motive, after the targets, that are instantiated with non-atomic expressions in the goal

        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              def Lean.Meta.altArity (motive : Expr) (n : Nat) :

              Given the type t of an alternative, determines the number of parameters (.forall and .let)-bound, and whether the conclusion is a motive-application.

              Equations
              Instances For
                def Lean.Meta.getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Lean.Meta.getElimInfo (elimName : Name) (baseDeclName? : Option Name := none) :
                  Equations
                  Instances For

                    Eliminators/recursors may have implicit targets. For builtin recursors, all indices are implicit targets. Given an eliminator and the sequence of explicit targets, this methods returns a new sequence containing implicit and explicit targets.

                    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
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lean.Meta.addCustomEliminator (declName : Name) (attrKind : AttributeKind) (induction : Bool) :
                            Equations
                            Instances For

                              Gets all the eliminators defined using the @[induction_eliminator] and @[cases_eliminator] attributes.

                              Equations
                              Instances For
                                def Lean.Meta.getCustomEliminator? (targets : Array Expr) (induction : Bool) :

                                Gets an eliminator appropriate for the provided array of targets. If induction is true then returns a matching eliminator defined using the @[induction_eliminator] attribute and otherwise returns one defined using the @[cases_eliminator] attribute.

                                The @[induction_eliminator] attribute is for the induction tactic and the @[cases_eliminator] attribute is for the cases tactic.

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