monae icon indicating copy to clipboard operation
monae copied to clipboard

Published 20 hours ago • verified publisher icon affeldt-aist

2023/6/30: SMCGlobal, SMCLocal and extract

Open snowmantw opened this issue 1 year ago • 1 comments

Goal: define SMCGlobal, SMCLocal and SMCLang.

snowmantw avatar Jun 29 '23 14:06 snowmantw

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).

snowmantw avatar Jun 29 '23 15:06 snowmantw