[GHC] #4385: Type-level natural numbers

[GHC]

#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