 Timestamp:
 Oct 10, 2011, 3:54:26 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/JMCoercions.ma
r1062 r1335 2 2 include "basics/types.ma". 3 3 include "basics/list.ma". 4 5 notation > "hvbox(a break ≃ b)"6 non associative with precedence 457 for @{ 'jmeq ? $a ? $b }.8 9 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"10 non associative with precedence 4511 for @{ 'jmeq $t $a $u $b }.12 13 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).14 15 lemma eq_to_jmeq:16 ∀A: Type[0].17 ∀x, y: A.18 x = y → x ≃ y.19 //20 qed.21 4 22 5 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. … … 38 21 qed. 39 22 40 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.41 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %42 qed.43 44 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.45 46 23 (* END RUSSELL **)
Note: See TracChangeset
for help on using the changeset viewer.