You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
My understanding is that one of the big improvements of cooltt over redtt is that cooltt implements the full eta-law for the disjunction on cofibrations. I'm having a hard time pinpointing where this occurs in the codebase. Maybe I just need to get better at reading OCaml. Could someone point me in the right spot? if the decision procedure is written down anywhere that would also be very helpful.
Does the decision procedure rely on cofbrations being in a disjunctive normal form?
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
My understanding is that one of the big improvements of cooltt over redtt is that cooltt implements the full eta-law for the disjunction on cofibrations. I'm having a hard time pinpointing where this occurs in the codebase. Maybe I just need to get better at reading OCaml. Could someone point me in the right spot? if the decision procedure is written down anywhere that would also be very helpful.
Does the decision procedure rely on cofbrations being in a disjunctive normal form?
Beta Was this translation helpful? Give feedback.
All reactions