@edwinbrady Is it intentional that something like this doesn't type check?
foo : (x : Bool) -> (x = True) -> Unit
foo x Refl = ()
-
Show this thread
-
Replying to @JadenGeller @edwinbrady
The equivalent in Agda also didn't check until relatively recently. It's now elaborated to something like `foo .True Refl = let x = True in ()`.
1 reply 0 retweets 1 like
Replying to @laMudri @JadenGeller
I was thinking Idris 2 should allow this. At the minute (in Idris 2) you can say 'foo x@_ Refl' and it's a fairly small step to allow it without the @ pattern.
9:48 AM - 3 Jan 2019
from Scotland, United Kingdom
0 replies
0 retweets
2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.