Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (9 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Plogic/equality.ma

    r260 r268  
    1717ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
    1818    refl: eq A x x.
    19    
     19
     20notation "hvbox(t⌈h ↦ o⌉)"
     21  with precedence 45
     22  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
     23 
    2024interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
    2125
Note: See TracChangeset for help on using the changeset viewer.