Changeset 374 for Deliverables/D4.1/Matita/Plogic

Timestamp:

Dec 5, 2010, 11:54:59 PM (10 years ago)

Author:

sacerdot

Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File:

• Deliverables/D4.1/Matita/Plogic/equality.ma (modified) (1 diff)

Deliverables/D4.1/Matita/Plogic/equality.ma

@@ -18 +18 @@
     refl: eq A x x.
 
-notation "hvbox(t⌈h ↦ o⌉)"
+notation "hvbox(t⌈o ↦ h⌉)"
   with precedence 45
   for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.