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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r709 r711 322 322 ]. 323 323 interpretation "integer multiplication" 'times x y = (Z_times x y). 324 (* Now in cerco/Util.ma325 (* Borrowed from standardlibrary/didactic/exercises/duality.ma with precedences tweaked *)326 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 }.327 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 }.328 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).329 *)330 324 (* datatypes/list.ma *) 331 325
Note: See TracChangeset
for help on using the changeset viewer.