narc-rs

narc-rs copied to clipboard

Discussion

8

Here's my initial thoughts about this language: + Conversion check should be nominal for simplicity + Only case-tree instantiation need to be supported + Surface syntax should be considerate of...

ice1000

I guess, probably I should write it myself, instead of trying to translate Agda.

ice1000

As title. http://hackage.haskell.org/package/Agda-2.5.4/docs/Agda-TypeChecking-Rules-Record.html

ice1000

https://docs.rs/console/0.9.1/console/struct.Emoji.html

ice1000

So it's more friendly for debugging Narc

ice1000

Currently, verbosity is just a bool switch. I think we can have more fine-grained verbosity level control

ice1000

Right now there's only unnamed dbi: https://github.com/owo-lang/narc-rs/blob/6fcbca28127212a5ca5883e6eaa310da6dfa3c4a/src/syntax/core/subst/dbi.rs#L14

ice1000

https://github.com/AndrasKovacs/elaboration-zoo/blob/af8f8e47768285e4ee5a10c2c2313c2768235279/04-implicit-args/Main.hs#L494

ice1000

Re-think about constructor and projection's telescope

2

As title.

ice1000

Check codatatypes' projections. After #16

ice1000