Documentation

Lean.Elab.Tactic.Impossible

impossible tactic #

source
def Lean.Elab.Tactic.elabImpossibleConfig (cfg : Syntax) (init : Parser.Tactic.ImpossibleConfig := { }) (logExceptions : Bool := true) :
TacticM Parser.Tactic.ImpossibleConfig
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.evalImpossible :
    Tactic
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For