Open Lysxia opened 4 years ago
mrec-fix is currently defined with a let (issue #170, PR #171), which, sadly, gets simplified away with cbn/simpl.
mrec-fix
let
cbn
simpl
One solution may be to make the D : Type -> Type argument explicit.
D : Type -> Type
mrec-fix
is currently defined with alet
(issue #170, PR #171), which, sadly, gets simplified away withcbn
/simpl
.One solution may be to make the
D : Type -> Type
argument explicit.