Jon Sterling

Parse errors?

3

@freebroccolo When the parser fails, I'd like it to emit some minimal message that tells me what went wrong; it doesn't need to be a good message (for instance, I...

Support for universe polymorphism

14

It would be game-changing to support universe polymorphism. Right now I have a class of large categories, and this is enough for me at the moment, but I would be...

Difficulty with `id_phant`

6

I am trying to define categories using HB and ran into a little issue that I wasn't sure how to deal with; am sorry if opening a ticket is not...

- https://github.com/RedPRL/cooltt/blob/master/src/core/TermBuilder.mli - https://github.com/RedPRL/cooltt/blob/master/src/core/Splice.mli

https://github.com/RedPRL/cooltt/blob/master/src/core/Tactic.ml#L95

Right now, this is only an elaborator; there is no notion of top-level declaration, and no parser.

Ability to configure which CM file is loaded

2

This is a great plugin! If one improvement were possible, I think I might be able to use it in my projects. The problem is that largescale SML developments typically...