Ignore:
Timestamp:
Nov 12, 2010, 4:51:45 PM (9 years ago)
Author:
mulligan
Message:

More functions on bitvectors written.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Nat.ma

    r236 r237  
    3434    ].
    3535   
    36 notation "n break ≤ m"
     36notation "hvbox(n break ≤ m)"
    3737  non associative with precedence 47
    3838  for @{ 'less_than_or_equal $n $m }.
     
    4949    n ≤ m.
    5050   
    51 notation "n break ≥ m"
     51notation "hvbox(n break ≥ m)"
    5252  non associative with precedence 47
    5353  for @{ 'greater_than_or_equal $n $m }.
     
    6262    m ≤ n ∧ ¬(m = n).
    6363   
    64 notation "n break < m"
     64notation "hvbox(n break < m)"
    6565  non associative with precedence 47
    6666  for @{ 'less_than $n $m }.
     
    7272    n < m.
    7373   
    74 notation "n break > m"
     74notation "hvbox(n break > m)"
    7575  non associative with precedence 47
    7676  for @{ 'greater_than $n $m }.
     
    8787    ].
    8888   
    89 notation "n break + m"
     89notation "hvbox(n break + m)"
    9090  right associative with precedence 52
    9191  for @{ 'plus $n $m }.
     
    103103    ].
    104104   
    105 notation "n break - m"
     105notation "hvbox(n break - m)"
    106106  right associative with precedence 47
    107107  for @{ 'minus $n $m }.
     
    119119    ].
    120120   
    121 notation "n break * m"
     121notation "hvbox(n break * m)"
    122122  right associative with precedence 47
    123123  for @{ 'multiplication $n $m }.
     
    142142      ].
    143143     
    144 notation "n break ÷ m"
     144notation "hvbox(n break ÷ m)"
    145145  right associative with precedence 47
    146146  for @{ 'division $n $m }.
     
    165165      ].
    166166   
    167 notation "n break % m"
     167notation "hvbox(n break % m)"
    168168  right associative with precedence 47
    169169  for @{ 'modulus $n $m }.
    170170 
    171171interpretation "Nat modulus" 'modulus m n = (modulus m n).
     172
     173ndefinition divide_with_remainder ≝
     174  λm, n: Nat.
     175    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
     176
     177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     178(* Exponentials, and square roots.                                            *)
     179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     180
     181nlet rec exponential (m: Nat) (n: Nat) on n ≝
     182  match n with
     183    [ Z ⇒ S (Z)
     184    | S o ⇒ m * exponential m o
     185    ].
     186   
     187notation "hvbox(n ^ m)"
     188  left associative with precedence 52
     189  for @{ 'exponential $n $m }.
     190 
     191interpretation "Nat exponential" 'exponential n m = (exponential n m).
    172192
    173193(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.