Documentation

Aesop.RuleTac.Cases

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
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          partial def Aesop.RuleTac.cases.go (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array Aesop.CtorNames) (newGoals : Array Aesop.Subgoal) (excluded : Array Lean.FVarId) (diff : Aesop.GoalDiff) (goal : Lean.MVarId) :