snowmantw
commented
1 year ago Check StateMonad.acto (VarName -> MonadSMCLocals F P VarName).
In environment
F, P : UU0
VarName : eqType
The term "VarName -> MonadSMCLocals F P VarName" has type
"Type@{max(Equality.type.u0,MonadSMCLocals.u0)}"
while it is expected to have type "Type@{monad_model.4448}"
(universe inconsistency: Cannot enforce MonadSMCLocals.u0 <=
monad_model.4448 because monad_model.4448 < isFunctor.axioms_.u0
<= MonadSMCLocal.axioms_.u3 <= MonadSMCLocal.type.u0 <= MonadSMCLocals.u0).
Goal: define SMCGlobal, SMCLocal and SMCLang.