-
Iavor S. Diatchki authored
Note 1: For the moment, we provide instances only for numbers that fit in a Word. The reason is a quite mundane: to generate evidence for arbitrary integers we need to generate integer literals. In the core syntax this is a monadic operation but the function that generates the core for evidence is pure. It would not be hard to monadify it but requires changes to a bunch of other functions so I thought it is better left for a separate change. Note 2: The evidence that we generate for a NatI is just a word. Technically, we should be generate a word with two coercions: one to turn it into a NatS and another to turn that into a NatI. Operationally, these do not do anything, but it would be better to fix this. I didn't do it yet because I need to look up how to make these coercions.
4715b871