RedPRL/sml-redprl

Print integers as (int i).

Closed this issue · 4 comments

favonia commented

Currently the printer is not a section of parser when it comes to integers. An easy solution is to print integers as (int i) where numbers by default will be dimension constants. It also makes (nat i) natural and solves #590 completely.

cangiuli commented

I'm OK with printing that way. Can you explain what this has to do with #590?

favonia commented

@cangiuli The practical reason why nat is a subtype of int is to allow users to write numerals for both types. If we are writing the numbers as (int 3) and (nat 3), then there is no need to make nat a subtype of int, and so their recursor can be reverted back to something more systematic. In other words, int can just be the normal nat + nat.

  • 👍1
favonia commented

(Why wasn't this issue closed automatically? I thought "Solve" is a keyword.)

jonsterling commented

@favonia I think it accepts "resolve", not sure about solve.