• Iavor S. Diatchki's avatar
    Add the built-in instances for class NatI. · 4715b871
    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
TcInteract.lhs 79.4 KB