Andrew Martin andrewsmartin

## Nat.scala
sealed trait Nat
class _0 extends Nat
class Succ[T <: Nat]() extends Nat
def Succ[T <: Nat] = new Succ[T]()

object NatOps {
  trait Sum[T <: Nat, U <: Nat] { type R <: Nat }
  type Aux[T <: Nat, U <: Nat, S <: Nat] = Sum[T, U] { type R = S }

  implicit def sum0[U <: Nat] = new Sum[_0, U] { type R = U }

## keybase.md

      
        
          
            
              
              1 file
            
          
          
            
              
              0 forks
            
          
          
            
              
              0 comments
            
          
          
            
              
              0 stars
            
          
        
        
          
              
          
          
            
                andrewsmartin
                / keybase.md
            
            
              Created
              April 5, 2016 17:03
            
          
        
      
        
  
      
    Keybase proof

I hereby claim:

I am andrewsmartin on github.
I am andrewsmartin (https://keybase.io/andrewsmartin) on keybase.
I have a public key ASB2hlo8jPdi1cK625D7AaAqXNVMxrI5F6P0dxzyHmw-OQo

To claim this, I am signing this object:
	sealed trait Nat
	class _0 extends Nat
	class Succ[T <: Nat]() extends Nat
	def Succ[T <: Nat] = new Succ[T]()

	object NatOps {
	trait Sum[T <: Nat, U <: Nat] { type R <: Nat }
	type Aux[T <: Nat, U <: Nat, S <: Nat] = Sum[T, U] { type R = S }

	implicit def sum0[U <: Nat] = new Sum[_0, U] { type R = U }