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

 5 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Arithmetic.ma
r475 r533 28 28 let cy_flag ≝ geb result_old (2^n) in 29 29 let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in 30 mk_pair ? ? (bitvector_of_nat n result)30 pair ? ? (bitvector_of_nat n result) 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 … … 111 111 Some ? (bitvector_of_nat n result) 112 112 ]. 113 114 alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)". 115 116 definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝ 113 114 definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ 117 115 λn. 118 116 match n with 
Deliverables/D3.1/Csemantics/cerco/BitVectorTrie.ma
r475 r533 1 include "basics/ sums.ma".1 include "basics/types.ma". 2 2 3 3 include "cerco/BitVector.ma". 
Deliverables/D3.1/Csemantics/cerco/Char.ma
r475 r533 1 1 (*include "logic/pts.ma".*) 2 2 3 include "core_notation.ma".4 3 include "basics/pts.ma". 5 4 
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 ≝ 
Deliverables/D3.1/Csemantics/cerco/Vector.ma
r475 r533 6 6 include "basics/list.ma". 7 7 include "basics/bool.ma". 8 include "basics/ sums.ma".8 include "basics/types.ma". 9 9 10 10 include "cerco/Util.ma". … … 159 159  VCons o he tl ⇒ λK. 160 160 match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with 161 [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉161 [ pair v1 v2 ⇒ 〈he:::v1, v2〉 162 162 ] 163 163 ] (?: (S (m' + n)) = S (m' + n))]. … … 269 269 λv: Vector A n. 270 270 λq: Vector B n. 271 zip_with A B (A × B) n ( mk_pair A B) v q.271 zip_with A B (A × B) n (pair A B) v q. 272 272 273 273 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.