Documentation

Aesop.RuleTac.Cases

Equations
Instances For
    Instances For
      Equations
      Instances For
        def Aesop.RuleTac.cases (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) :
        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
            partial def Aesop.RuleTac.cases.go (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) (newGoals : Array Subgoal) (excluded : Array Lean.FVarId) (diff : GoalDiff) (goal : Lean.MVarId) :