Documentation

Lean.Meta.Tactic.ElimInfo

  • name : Lake.Name
  • declName? : Option Lake.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

    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.

    Instances For
      Equations
      def Lean.Meta.altArity (motive : Lean.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
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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
              partial def Lean.Meta.addImplicitTargets.collect (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (type : Lean.Expr) (argIdx : Nat) (targetIdx : Nat) (implicits : Array Lean.MVarId) (targets' : Array Lean.Expr) :
              Instances For
                Equations
                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Lean.Meta.addCustomEliminator (declName : Lake.Name) (attrKind : Lean.AttributeKind) (induction : Bool) :
                    Equations
                    Instances For

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

                      Equations
                      Instances For

                        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