non-exhaustive for meta

Stream: general

[Zesen Qian]

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

[Simon Hudon]

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]

Whenever you would leave some cases out, it is a good practice to write an error message instead

[Simon Hudon]

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

[Zesen Qian]

@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]

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]

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

[Simon Hudon]

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)

[Zesen Qian]

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

prog : hint -> pexpr

[Zesen Qian]

because the generation of the proof doesn't depends on inspection of the prover's environment, but only on the hint.

[Simon Hudon]

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

[Gabriel Ebner]

There is also undefined_core "my error message"

[Zesen Qian]

@Gabriel Ebner I think that's what I wanted.