Zulip Chat Archive

Stream: general

Topic: non-exhaustive for meta


view this post on Zulip Zesen Qian (Jul 09 2018 at 20:29):

If we allow non-termination at meta level, shouldn't we also allow non-exhaustive match?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 09 2018 at 20:34):

You're making clear to any reader that you don't accept every input

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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 tactic

view this post on Zulip 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 tactic because tactic is meta)

view this post on Zulip Zesen Qian (Jul 09 2018 at 21:05):

hmm, what about a meta-program that simply returns a proof?

prog : hint -> pexpr

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 09 2018 at 21:08):

You can return a default value like ``(Type)

view this post on Zulip Gabriel Ebner (Jul 09 2018 at 21:08):

There is also undefined_core "my error message"

view this post on Zulip 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