search

RedPRL / cooltt

😎TT
http://www.redprl.org/
Apache License 2.0
217 stars 16 forks source link

🙈 Implicit Cofibration Proofs #382

Closed mmcqd closed 2 years ago

mmcqd commented 2 years ago

(emoji needed)

This PR makes functions out of cofibration proofs implicit. So to inhabit [Ï•] -> A we can simply write down an element of A and it will be elaborated to a function. Similarly, if we have f : [Ï•] -> A, it will be elaborated to f *.

The main thing this is lacking is nice printing. We still print( functions out of) and (applications to) cofibration proofs, because we do not have types when printing. Not printing applications to * is straightforward, but conditionally not printing lambdas is more difficult. We may need to add separate core terms for these constructs.

Regardless of printing, I think having these proofs clutter only the core is superior to having them clutter both the surface language and the core.

jonsterling commented 2 years ago

@mmcqd Wow cool! I will try to have a look at this within the next 48 hours. I think it is fair to say that having the output of cooltt be valid cooltt code is not currently one of the invariants that we satisfy, so I would not hold up the PR for the sake of that.