search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

add bool paths, DNE, LEM, aux proofs, refactor #447

Closed clayrat closed 5 years ago

jonsterling commented 5 years ago

@clayrat Wow, this is super cool! At redtt HQ, we're all super impressed with how you pulled this together :sunglasses:

clayrat commented 5 years ago

Made the changes, so should I also remove happly and apd? I must say the inlined version with apd does look more verbose, since you have to at least mention the path twice.

jonsterling commented 5 years ago

@clayrat OK, let's leave apd in for now (maybe we'll revisit it later), but let's remove happly.

clayrat commented 5 years ago

@jonsterling removed