google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

remove Prop kind and associated cruft #32

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
type

prompt> :pre

you see:

data Prop :: *1 where
  Success :: Prop
and:: Prop ~> Prop ~> Prop
{and Success x } = x

these can be removed, since there is no Prop kind any more,
propositions are handled internally in a different way.

Original issue reported on code.google.com by ggr...@gmail.com on 8 Nov 2007 at 11:34

GoogleCodeExporter commented 9 years ago
the users' guide mentions Prop, Success and "and" on pages 3 and 5

Original comment by ggr...@gmail.com on 12 Nov 2007 at 11:22

GoogleCodeExporter commented 9 years ago
the Bind type is another candidate, need to browse the sources to see what it 
is designed for. It is not occurring in the manual.

Original comment by ggr...@gmail.com on 18 Nov 2007 at 11:23

GoogleCodeExporter commented 9 years ago
it is indeed possible to access the Prop and Success kinds,

prompt> :k (Int == Char)
(Int == Char) :: Prop  = {(==) Int Char}
prompt> :k Success
Success :: Prop

prompt> :no {and Success Success}

   {and Success Success}
Normalizes to:
  Success
Refinement:

-----------------
on the remove-Prop branch I tried to remove "Prop" but it turns out,
that this *is* part of the internal machinery. It would be still
interesting to come up with an interesting use case for (==)
and possibly (!=) too.

Then these should be documented in the manual.

Original comment by ggr...@gmail.com on 4 Dec 2007 at 3:25

GoogleCodeExporter commented 9 years ago
Revision 43 removed 'Bind' (on the branches/general-cleanups branch)

Original comment by ggr...@gmail.com on 8 Dec 2007 at 11:14

GoogleCodeExporter commented 9 years ago
r153 merges e.g. r43 to trunk.

Some really unneeded constructs should be gone now. Closing.

Original comment by ggr...@gmail.com on 1 Aug 2008 at 2:43

GoogleCodeExporter commented 9 years ago
ok.

Original comment by ggr...@gmail.com on 3 Feb 2011 at 10:28