G. Allais
G. Allais
Minimised: ```idris %default total data View : Nat -> Type where Plus : (k, l : Nat) -> View (k + l) view : View m -> Void view {m...
AFAICT it's unambiguous so I'm not too fussed about it. If someone wants to look into having stricter rules for indentation levels in `Idris.Parser`'s `letBinder` I won't oppose it.
I see. The issue is that `{` can be used to delimit a block instead of indentation. So in theory you could write (it seems broken at the moment for...
Note that you can implement ``` recover : @0 ⊥ → ⊥ recover () ``` so you can plug your contradiction into a call to `⊥-elim`.
There's also the issue of `Irrelevant` vs. `@0` annotation. I don't think we have anything `@0`-related in the lib at the minute.
I suspect it's due to the checker seeing the Bool is 0 and so it assumes the pattern must have been forced by another split. Except that we are in...
Related idea: Coq's [constructive epsilon](https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html) module.
It's called [Markov's Principle](https://en.wikipedia.org/wiki/Markov%27s_principle)
Axioms are never safe
My reponse was purely technical: it cannot be accepted by `--safe`. That being said, I am more than happy to have it in the stdlib (together with its properties).