Changeset 2796 for src/utilities


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r2309 r2796  
    204204for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
    205205        λ${ident E}.$s ] (refl ? $t) }.
     206
     207inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     208    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     209
     210interpretation "exists in Type[1]" 'exists_Type1 x = (ex_Type1 ? x).
     211
     212notation < "hvbox(∃\sub 1 ident i : ty break . p)"
     213 right associative with precedence 20
     214for @{'exists_Type1 (\lambda ${ident i} : $ty. $p) }.
     215
     216notation > "\exists[1] list1 ident x sep , opt (: T). term 19 Px"
     217  with precedence 20
     218  for ${ default
     219          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}:$T.$acc)} } }
     220          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}.$acc)} } }
     221       }.
Note: See TracChangeset for help on using the changeset viewer.