Changeset 697 for src/ASM/Util.ma
Legend:
- Unmodified
- Added
- Removed
-
src/ASM
-
Property
svn:mergeinfo
set to
(toggle deleted branches)
/src/Clight/cerco merged eligible /Deliverables/D3.1/C-semantics/cerco 531-693 /Deliverables/D4.1/Matita/new-matita-development 476-530
-
Property
svn:mergeinfo
set to
(toggle deleted branches)
-
src/ASM/Util.ma
r690 r697 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 ≝ … … 13 13 ]. 14 14 15 (* 15 16 notation "hvbox('if' b 'then' t 'else' f)" 16 17 non associative with precedence 83 17 18 for @{ 'if_then_else $b $t $f }. 19 *) 20 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 21 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. 18 22 19 23 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). … … 27 31 28 32 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 33 34 let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝ 35 match l with 36 [ nil ⇒ r 37 | cons h t ⇒ revapp T t (h::r) 38 ]. 39 40 definition rev ≝ λT:Type[0].λl. revapp T l [ ]. 29 41 30 42 lemma eq_rect_Type0_r : … … 64 76 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 65 77 with precedence 10 66 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.78 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 67 79 68 80 notation "⊥" with precedence 90 … … 100 112 101 113 let rec division_aux (m: nat) (n : nat) (p: nat) ≝ 102 match ltb n pwith114 match ltb n (S p) with 103 115 [ true ⇒ O 104 116 | false ⇒ … … 147 159 definition divide_with_remainder ≝ 148 160 λm, n: nat. 149 mk_pair ? ? (m ÷ n) (modulus m n).161 pair ? ? (m ÷ n) (modulus m n). 150 162 151 163 let rec exponential (m: nat) (n: nat) on n ≝
Note: See TracChangeset
for help on using the changeset viewer.