Changeset 711


Ignore:
Timestamp:
Mar 27, 2011, 3:06:13 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r709 r711  
    322322].
    323323interpretation "integer multiplication" 'times x y = (Z_times x y).
    324 (* Now in cerco/Util.ma
    325 (* Borrowed from standard-library/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 *)
    330324(* datatypes/list.ma *)
    331325
Note: See TracChangeset for help on using the changeset viewer.