Changeset 711 for src/utilities

Timestamp:

Mar 27, 2011, 3:06:13 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• src/utilities/extralib.ma (modified) (1 diff)

src/utilities/extralib.ma

@@ -322 +322 @@
 ].
 interpretation "integer multiplication" 'times x y = (Z_times x y).
-(* Now in cerco/Util.ma
-(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
-notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
-*)
 (* datatypes/list.ma *)