Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
constants with the same names
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 22 Jun 2011 17:57:15 +0900
changeset 2884 0599286b1e2a
parent 2883 05a4745b0a9d
child 2885 1264f2a21ea9
constants with the same names
Attic/FIXME-TODO file | annotate | diff | comparison | revisions 
--- a/Attic/FIXME-TODO	Wed Jun 22 04:49:56 2011 +0900
+++ b/Attic/FIXME-TODO	Wed Jun 22 17:57:15 2011 +0900
@@ -24,6 +24,11 @@
     typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
       morphisms list_of_dlist Abs_dlist
 
+- Allow defining constants with existing names.
+    Since 'insert' is defined for sets,
+    "quotient_definition insert" fails for fset
+    however "definition" succeeds.
+
 Lower Priority
 ==============
nominal2