add more examples to Domain_ex.thy
authorhuffman
Tue, 21 Apr 2009 17:07:44 -0700
changeset 30922 96d053e00ec0
parent 30921 fbdefa2196fa
child 30976 44637646fa17
child 30993 796cee3729f0
child 31004 ac7e90792089
add more examples to Domain_ex.thy
src/HOLCF/ex/Domain_ex.thy
--- a/src/HOLCF/ex/Domain_ex.thy	Tue Apr 21 17:02:48 2009 -0700
+++ b/src/HOLCF/ex/Domain_ex.thy	Tue Apr 21 17:07:44 2009 -0700
@@ -203,4 +203,19 @@
   -- "Tactic failed."
 *)
 
+text {* Declaring class constraints on the LHS is currently broken. *}
+(*
+domain ('a::cpo) box = Box (lazy 'a)
+  -- "Malformed YXML encoding: multiple results"
+*)
+
+text {*
+  Class constraints on the RHS are not supported yet.  This feature is
+  planned to replace the old-style LHS class constraints.
+*}
+(*
+domain 'a box = Box (lazy "'a::cpo")
+  -- {* Inconsistent sort constraint for type variable "'a" *}
+*)
+
 end