Changeset 697 for src/ASM/Util.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Author:
campbell
Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM

  • src/ASM/Util.ma

    r690 r697  
    11include "arithmetics/nat.ma".
    22include "basics/list.ma".
    3 include "basics/sums.ma".
     3include "basics/types.ma".
    44
    55definition if_then_else ≝
     
    1313  ].
    1414   
     15(*
    1516notation "hvbox('if' b 'then' t 'else' f)"
    1617  non associative with precedence 83
    1718  for @{ 'if_then_else $b $t $f }.
     19*)
     20notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     21notation < "'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 }.
    1822
    1923interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
     
    2731
    2832definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
     33
     34let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
     35match l with
     36[ nil ⇒ r
     37| cons h t ⇒ revapp T t (h::r)
     38].
     39
     40definition rev ≝ λT:Type[0].λl. revapp T l [ ].
    2941
    3042lemma eq_rect_Type0_r :
     
    6476notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    6577 with precedence 10
    66 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
     78for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    6779
    6880notation "⊥" with precedence 90
     
    100112
    101113let rec division_aux (m: nat) (n : nat) (p: nat) ≝
    102   match ltb n p with
     114  match ltb n (S p) with
    103115    [ true ⇒ O
    104116    | false ⇒
     
    147159definition divide_with_remainder ≝
    148160  λm, n: nat.
    149     mk_pair ? ? (m ÷ n) (modulus m n).
     161    pair ? ? (m ÷ n) (modulus m n).
    150162   
    151163let rec exponential (m: nat) (n: nat) on n ≝
Note: See TracChangeset for help on using the changeset viewer.