Changeset 1598 for src/ASM/Util.ma
 Timestamp:
 Dec 12, 2011, 5:53:36 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1516 r1598 688 688 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" 689 689 with precedence 90 for @{ 'triple $a $b $c}. 690 interpretation "Triple construction" 'triple x y z = ( pair ? ? (pair? ? x y) z).690 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z). 691 691 692 692 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" 693 693 with precedence 90 for @{ 'quadruple $a $b $c $d}. 694 interpretation "Quadruple construction" 'quadruple w x y z = ( pair ? ? (pair ? ? w x) (pair? ? y z)).694 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)). 695 695 696 696 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" … … 802 802 definition divide_with_remainder ≝ 803 803 λm, n: nat. 804 pair ? ?(m ÷ n) (modulus m n).804 mk_Prod … (m ÷ n) (modulus m n). 805 805 806 806 let rec exponential (m: nat) (n: nat) on n ≝
Note: See TracChangeset
for help on using the changeset viewer.