Changeset 1335


Ignore:
Timestamp:
Oct 10, 2011, 3:54:26 PM (8 years ago)
Author:
sacerdot
Message:

Ported to new Matita stdlib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/JMCoercions.ma

    r1062 r1335  
    22include "basics/types.ma".
    33include "basics/list.ma".
    4 
    5 notation > "hvbox(a break ≃ b)"
    6   non associative with precedence 45
    7 for @{ 'jmeq ? $a ? $b }.
    8 
    9 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    10   non associative with precedence 45
    11 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.
    214
    225definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     
    3821qed.
    3922
    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 
    4623(* END RUSSELL **)
Note: See TracChangeset for help on using the changeset viewer.