Changeset 533 for Deliverables/D3.1/Csemantics/cerco/Util.ma
 Timestamp:
 Feb 16, 2011, 4:25:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Util.ma
r475 r533 1 1 include "arithmetics/nat.ma". 2 2 include "basics/list.ma". 3 include "basics/ sums.ma".3 include "basics/types.ma". 4 4 5 5 definition if_then_else ≝ … … 28 28 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 29 29 30 let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝ 31 match l with 32 [ nil ⇒ r 33  cons h t ⇒ revapp T t (h::r) 34 ]. 35 36 definition rev ≝ λT:Type[0].λl. revapp T l [ ]. 37 30 38 lemma eq_rect_Type0_r : 31 39 ∀A: Type[0]. … … 64 72 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 65 73 with precedence 10 66 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.74 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 67 75 68 76 notation "⊥" with precedence 90 … … 147 155 definition divide_with_remainder ≝ 148 156 λm, n: nat. 149 mk_pair ? ? (m ÷ n) (modulus m n).157 pair ? ? (m ÷ n) (modulus m n). 150 158 151 159 let rec exponential (m: nat) (n: nat) on n ≝
Note: See TracChangeset
for help on using the changeset viewer.