Auke Booij
Auke Booij
```graphql query MyQuery { test(limit: 2147483648) { id } } ``` yields: ```json { "errors": [ { "extensions": { "path": "$.selectionSet.test.args.limit", "code": "parse-failed" }, "message": "The value 2.147483648e9 lies outside...
#1137 defined a type of positive naturals in [`theories/Spaces/Pos/Core.v`](https://github.com/HoTT/HoTT/blob/7910fb7fe6390320438608a5480b5947f66d4eb6/theories/Spaces/Pos/Core.v#L8): ```coq Inductive Pos : Type0 := | xH : Pos | x0 : Pos -> Pos | x1 : Pos ->...
The error message for type checking errors, while correct, is rather unhelpful in bigger proofs. It would be nice if it could at least state a line number where things...
``` module test where import nat suc' : nat -> nat = suc ``` yields: ``` Type checking failed: expected a data type for the constructor suc but got Pi...
Although the C client side is progressing steadily (reimplementing the C ABI), there is no clear API for haskellers to use. The library should stay flexible, but that doesn't mean...
The .CABI modules implement the C ABI. While the client side is progressing steadily, the server side has yet to be written. Writing a server side is useful because it...
This is slowly becoming a fairly serious project, so it probably contains several pieces of code that really should be generalised and released as standalone packages. I don't know what...
It would be nice to have some unit testing and quickcheck-based property testing for our library. The libwayland developers are currently struggling to do anything in this direction, so this...
[This](http://tab.snarc.org/posts/haskell/2017-03-20-compilation-cstruct.html) looks kinda neat.