search

RedPRL / cooltt

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

dimension inequality #369

Closed jonsterling closed 2 years ago

jonsterling commented 2 years ago

This is extremely slow and badly written. The 🧞 has returned!

jonsterling commented 2 years ago

I seem to have broken everything LOL. Probably due to some mistake in my incompetent editing of the kado library.

jonsterling commented 2 years ago

I Upgraded to the new branch! 😎 Right now cooltt thinks that all propositions are true 😝

jonsterling commented 2 years ago

looks like you fixed it LOL

favonia commented 2 years ago

Alright I'm not super motivated to somehow print "i <= j && j <= i" as "i = j". At least not until cooltt has serious formalization.

jonsterling commented 2 years ago

I am also not motivated to worry about that...

On May 26, 2022, at 6:27 PM, favonia @.***> wrote:

Alright I'm not super motivated to somehow print "i <= j && j <= i" as "i = j". At least not until cooltt has serious formalization.

— Reply to this email directly, view it on GitHub https://github.com/RedPRL/cooltt/pull/369#issuecomment-1138756542, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAANOEJK2FX54FIETOXYZ43VL6Q7NANCNFSM5WFEHQKQ. You are receiving this because you authored the thread.