Changeset 268 for Deliverables/D4.1/Matita/Plogic
- Timestamp:
- Nov 23, 2010, 5:44:42 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Plogic/equality.ma
r260 r268 17 17 ninductive eq (A:Type[2]) (x:A) : A → Prop ≝ 18 18 refl: eq A x x. 19 19 20 notation "hvbox(t⌈h ↦ o⌉)" 21 with precedence 45 22 for @{ match (? : $o=$h) with [ refl ⇒ $t ] }. 23 20 24 interpretation "leibnitz's equality" 'eq t x y = (eq t x y). 21 25
Note: See TracChangeset
for help on using the changeset viewer.