Documentation

Lean.Elab.Tactic.Do.ProofMode.Cases

source
def Lean.Elab.Tactic.Do.ProofMode.synthIsAnd (σs H : Expr) :
OptionT MetaM (Expr × Expr × Expr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.Do.ProofMode.mCasesAddGoal (goals : IO.Ref (Array MVarId)) (σs T Q H : Expr) :
    MetaM (Unit × MGoal × Expr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.Do.ProofMode.mCasesExists {α : Type} (H : Expr) (name : TSyntax `Lean.binderIdent) (k : Expr → MetaM (α × MGoal × Expr)) :
      MetaM (α × MGoal × Expr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        partial def Lean.Elab.Tactic.Do.ProofMode.mCasesCore {α : Type} (σs H : Expr) (pat : Parser.Tactic.MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)) :
        MetaM (α × MGoal × Expr)
        source
        def Lean.Elab.Tactic.Do.ProofMode.elabMCases :
        Tactic
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For