#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by simonpj):
Iavor: what's your plan for this? I'd like to have it in the HEAD, but we
need to resolve the design issues first. Also I'm unsure about whether
you are actively developing or whether you've moved on to other things.
Oh, one other thing that isn't clear to me is how all this fits in FC. If
a Pressburger solver shows that (a*b = b*a), say how is that expressed as
a FC proof term?
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
