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

Timestamp:

Nov 23, 2010, 5:44:42 PM (10 years ago)

Author:

sacerdot

Message:

• notation moved to proper places
• new function split on Vectors

File:

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

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

@@ -17 +17 @@
 ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x.
-    
+
+notation "hvbox(t⌈h ↦ o⌉)"
+  with precedence 45
+  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
+ 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).