Changeset 533


Ignore:
Timestamp:
Feb 16, 2011, 4:25:00 PM (6 years ago)
Author:
campbell
Message:

Make stuff from D4.1 work with my copy of matita.

Location:
Deliverables/D3.1/C-semantics/cerco
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Arithmetic.ma

    r475 r533  
    2828    let cy_flag ≝ geb result_old (2^n) in
    2929    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)
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
     
    111111        Some ? (bitvector_of_nat n result)
    112112    ].
    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     
     114definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    117115  λn.
    118116    match n with
  • Deliverables/D3.1/C-semantics/cerco/BitVectorTrie.ma

    r475 r533  
    1 include "basics/sums.ma".
     1include "basics/types.ma".
    22
    33include "cerco/BitVector.ma".
  • Deliverables/D3.1/C-semantics/cerco/Char.ma

    r475 r533  
    11(*include "logic/pts.ma".*)
    22
    3 include "core_notation.ma".
    43include "basics/pts.ma".
    54
  • Deliverables/D3.1/C-semantics/cerco/Util.ma

    r475 r533  
    11include "arithmetics/nat.ma".
    22include "basics/list.ma".
    3 include "basics/sums.ma".
     3include "basics/types.ma".
    44
    55definition if_then_else ≝
     
    2828definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
    2929
     30let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
     31match l with
     32[ nil ⇒ r
     33| cons h t ⇒ revapp T t (h::r)
     34].
     35
     36definition rev ≝ λT:Type[0].λl. revapp T l [ ].
     37
    3038lemma eq_rect_Type0_r :
    3139  ∀A: Type[0].
     
    6472notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    6573 with precedence 10
    66 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
     74for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    6775
    6876notation "⊥" with precedence 90
     
    147155definition divide_with_remainder ≝
    148156  λm, n: nat.
    149     mk_pair ? ? (m ÷ n) (modulus m n).
     157    pair ? ? (m ÷ n) (modulus m n).
    150158   
    151159let rec exponential (m: nat) (n: nat) on n ≝
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r475 r533  
    66include "basics/list.ma".
    77include "basics/bool.ma".
    8 include "basics/sums.ma".
     8include "basics/types.ma".
    99
    1010include "cerco/Util.ma".
     
    159159      | VCons o he tl ⇒ λK.
    160160        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〉
    162162        ]
    163163      ] (?: (S (m' + n)) = S (m' + n))].
     
    269269  λv: Vector A n.
    270270  λ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.
    272272
    273273(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.