Steve Dunham
Steve Dunham
So this compiles fine: ```idris data Heap : (fs : Maybe a) -> Type where data Instr : Heap ht -> Type where Load : Instr hp ``` but this...
I've noticed that before. It looks like comments interfere with the handling for trailing parens too: ```idris five : Nat -> Nat five x = (case x of y =>...
And there also is splitting on `n` here: ```idris six : Nat -> Nat -> Nat six n {- n -} m = ?rhs7 ```
Nested functions get lifted to the top and get a bunch of extra arguments up front for the scope. Inside the function that nests it, the name is replaced by...
I'd been using 8.12, but I downloaded a copy of racket 8.13 for mac and it has the exe command: ``` % /Applications/Racket\ v8.13/bin/raco Usage: raco ... ... Frequently used...
I see the comment there. I'm using the upstream distribution, so I haven't seen this. We might want to make a note in our `INSTALL.md` around line 52 to let...
The issue here is subtle. It doesn't know which `length` to use because it doesn't know the type of `smth`. Your top level example is using `Smth` rather than `smth`...
Oh, I see. We don't get the warning because the warning is only for names in global scope.
Possibly related to #2513, which calls them irrefutable. (That issue is about `let` though.)
There is a `fromList` which does the opposite of `SortedMap.toList`. Should we change the name of that (and maybe `fromListWith` too)?