Changeset 2700 for src/ASM/Util.ma


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (7 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2673 r2700  
    784784    mk_Prod … (m ÷ n) (modulus m n).
    785785   
    786 let rec exponential (m: nat) (n: nat) on n ≝
    787   match n with
    788     [ O ⇒ S O
    789     | S o ⇒ m * exponential m o
    790     ].
    791 
    792 interpretation "Nat exponential" 'exp n m = (exponential n m).
    793    
    794786notation "hvbox(a break ⊎ b)"
    795787 left associative with precedence 55
Note: See TracChangeset for help on using the changeset viewer.