In Lean's logic, Lean.Parser.Term.panic : term
`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
`α` implements `Inhabited`.
At runtime, `msg` and the file position are printed to stderr unless the C
function `lean_set_panic_messages(false)` has been executed before. If the C
function `lean_set_exit_on_panic(true)` has been executed before, the process is
then aborted.
panic!
is equivalent to the default value specified in its type's Inhabited
instance.
This means that the type must have such an instance—a Nonempty
instance combined with the axiom of choice would render the program non-computable.
Products have the right instance:
example : Nat × String := panic! "Cant' find it"
Sums do not, by default:
example : Nat ⊕ String := failed to synthesize
Inhabited (Nat ⊕ String)
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
panic! "Cant' find it"
failed to synthesize
Inhabited (Nat ⊕ String)
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
The desired instance can be made available to instance synthesis using Lean.Parser.Term.have : term
`have` is used to declare local hypotheses and opaque local definitions.
It has the same syntax as `let`, and it is equivalent to `let +nondep`,
creating a *nondependent* let expression.
have
:
example : Nat ⊕ String :=
have : Inhabited (Nat ⊕ String) := Sum.inhabitedLeft
panic! "Cant' find it"