Binary for Windows

Add keywords unmatchable, axiom.

data Bool : U where 
| true : ... 
| false : ...

unmatchable data Interval : U where 
| i0 : ... 
| i1 : ...

axiom def max (i j : Interval) : Interval 
| i0 i0 = i0
| _  _  = i1

#eval max i0 i1

-- This is ok
def reflTrue (i : Interval) : Bool 
| i = true

-- -- This is an error
-- def trueToFalse (i : Interval) : Bool
-- | i0 = true 
-- | i1 = false

higher inductive S1 : U where 
| base : ... 
| loop : (i : Interval) -> ... 
    when 
    | i0 = base 
    | i1 = base