Comp. Exp3 ::= "comp" Exp4 Exp4 System ;
Fill. Exp3 ::= "fill" Exp4 Exp4 System ;
Glue. Exp3 ::= "glue" Exp4 System ;
--- GlueElem. Exp3 ::= "glueElem" Exp4 System ;
+GlueElem. Exp3 ::= "glueElem" Exp4 System ;
-- CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ;
-- GlueLine. Exp3 ::= "glueLine" Formula Formula Exp4 ;
-- GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ;
CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
<*> mapM resolveFormula phis
_ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
- IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
- Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
- Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
- Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
- -- GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
+ IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
+ Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+ Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+ Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
+ GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
-- GlueLine phi psi u ->
-- CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi
-- GlueLineElem phi psi u ->