Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (9 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/proper.ma

    r1635 r1640  
    1919  @{'proper_contra $r $s}.
    2020
    21 interpretation "is proper" 'is_proper f p = (p f f).
    22 notation "f ⊨ p" with precedence 50 for @{'is_proper $f $p}.
     21(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
     22notation > "f ⊨ p " with precedence 50 for @{$p $f $f}.
Note: See TracChangeset for help on using the changeset viewer.