Topic: non-exhaustive for meta
Zesen Qian (Jul 09 2018 at 20:29):
If we allow non-termination at meta level, shouldn't we also allow non-exhaustive match?
Simon Hudon (Jul 09 2018 at 20:32):
There are a lot of possibilities. While mandatory termination is very restrictive, exhaustiveness is not and it has great benefits. It allows Lean to tell you when you're messing up
Simon Hudon (Jul 09 2018 at 20:33):
Whenever you would leave some cases out, it is a good practice to write an error message instead
Simon Hudon (Jul 09 2018 at 20:34):
You're making clear to any reader that you don't accept every input
Zesen Qian (Jul 09 2018 at 21:01):
@Simon Hudon by error message you mean type level error? or is there some backdoor at meta-level that I can just halt the program in case of non-exhaustion?
Zesen Qian (Jul 09 2018 at 21:02):
because I'm pretty sure the rest case is not going to happen(and if it happens, that means problem in my meta-code).
Simon Hudon (Jul 09 2018 at 21:04):
If you're in
tactic, you can use
fail my_error_message to report the error ... it might actually a good enough reason to write code in
Simon Hudon (Jul 09 2018 at 21:05):
But that's not a backdoor, you can write trusted code in a similar way (but with different monads than
Zesen Qian (Jul 09 2018 at 21:05):
hmm, what about a meta-program that simply returns a proof?
prog : hint -> pexpr
Zesen Qian (Jul 09 2018 at 21:06):
because the generation of the proof doesn't depends on inspection of the prover's environment, but only on the hint.
Simon Hudon (Jul 09 2018 at 21:08):
You can return a default value like
Gabriel Ebner (Jul 09 2018 at 21:08):
There is also
undefined_core "my error message"
Zesen Qian (Jul 09 2018 at 21:09):
@Gabriel Ebner I think that's what I wanted.
Last updated: May 16 2021 at 05:21 UTC