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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 ≝
Note: See TracChangeset for help on using the changeset viewer.