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
Instances For
    source
    def Lean.Elab.Tactic.evalImpossible :
    Tactic
    Instances For