Adding warnings in Lean4

Stream: new members

[Michael Wahlberg]

How does one add warnings in a lean code when we know the user has inputted a false value? For example, I want my program to exit when someone inputs an empty list in this function :-

def non_empty(l : List ℕ) : Bool :=
  match l with
  | [] =>
  panic! "list is empty"
  | head :: tail => true

I read somewhere that panic works, but how exactly does it work?

[Adam Topaz]

panic! will just return the default value of the required type (so it requires an Inhabited instance for the return type, which Bool has).

[Adam Topaz]

But when you evaluate it at the empty case, it will give an error.

[Mario Carneiro]

You should not use panic! like this. It is allowed to be optimized away, so you cannot use it for anything except as a best effort way to catch implementation bugs

[Mario Carneiro]

Functions in lean are required to be total. If you want to report an error, use a return type like Except String Bool or IO Bool that allows you to report errors