Open ysharoda opened 4 years ago
This piece of code is accepted by the checker. Notice the use of + in the definition of assoc, although it is not defined.
theory Empty = ❚ diagram Carrier := ?Empty EXTEND { U : sort} ❚ diagram Pointed := ?Carrier_pres EXTEND { e : tm U } ❚ diagram Pointed0 := ?Pointed RENAME {e ⟿ 0} ❚ diagram Magma := ?Carrier_pres EXTEND {op : tm U ⟶ tm U ⟶ tm U } ❚ // # nt"1 %s 2" ❚ diagram Semigroup := ?Magma_pres EXTEND { assoc : ⊦ forall U [x y z : tm U] ≐ U ((x + y) + z) (x + (y + z)) } ❚
This piece of code is accepted by the checker. Notice the use of + in the definition of assoc, although it is not defined.