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

use cap tactic in paths.s2 #470

Closed ecavallo closed 5 years ago

ecavallo commented 5 years ago

It's not a performance win (s2/decode actually takes much more time to check now) but the normal forms are shorter.

ecavallo commented 5 years ago

This incidentally made it easier to define the oloop line of equivalences directly instead of using is-equiv/prop, which improves checking time considerably.