Opened this issue 4 years ago · 0 comments
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