Changeset 1598 for src/ASM/Util.ma


Ignore:
Timestamp:
Dec 12, 2011, 5:53:36 PM (8 years ago)
Author:
mulligan
Message:

changes over the last couple of days

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1516 r1598  
    688688notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
    689689with precedence 90 for @{ 'triple $a $b $c}.
    690 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
     690interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
    691691
    692692notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
    693693with precedence 90 for @{ 'quadruple $a $b $c $d}.
    694 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
     694interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
    695695
    696696notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
     
    802802definition divide_with_remainder ≝
    803803  λm, n: nat.
    804     pair ? ? (m ÷ n) (modulus m n).
     804    mk_Prod … (m ÷ n) (modulus m n).
    805805   
    806806let rec exponential (m: nat) (n: nat) on n ≝
Note: See TracChangeset for help on using the changeset viewer.