Binary for Windows

HIT (no boundary check yet)

data N : U where  
| zero : ...  
| succ : (pre : N) -> ...  

higher inductive Int : U where 
| pos : (n : N) -> ... 
| neg : (n : N) -> ... 
    when 
    | zero = pos zero

#eval neg zero -- pos zero

def abs (n : Int) : N where 
| pos n = n
| neg n = n