Binary

Termination Check 🎉

Binary for Windows

Refactor code. Fix bugs. And mutual recursion.

Binary for Windows

Start REPL with

> ./shitt repl 
shitt> 

---

Import a shitt file with

#load "FilePath.shitt"

-- here you can use anything defined in the file.

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

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 

Binary for Windows

Without K!

data Id {A : U} : (x y : A) -> U where 
| refl : (t : A) -> ... t t 

-- OK
fun uip {B : U} {x x1 : B} (p q: Id x x1) : Id {Id x x1} p q where 
| (refl _) (refl _) = refl (refl _)

-- OK
fun K {A : U} {a : A} (P : Id a a -> U) (p : P (refl _)) (e : Id a a) : P e where 
| P p (refl _) = p

-- OK
fun J {A : U} {a : A} (P : (b : A) -> Id a b -> U) (p : P a (refl _)) (b : A) (e : Id a b) : P b e 
| P p a (refl _) = p 

#withoutK

-- not OK
fun K1 {A : U} {a : A} (P : Id a a -> U) (p : P (refl _)) (e : Id a a) : P e where 
| P p (refl _) = p

-- not OK
fun uip1 {B : U} {x x1 : B} (p q: Id x x1) : Id {Id x x1} p q where 
| (refl _) (refl _) = refl (refl _)

-- not OK
fun weakK 
  {A : U} {a : A} 
  (P : Id {Id a a} (refl _) (refl _) -> U) 
  (p : P (refl _)) (e : Id {Id a a} (refl _) (refl _))
: P e where 
| P p (refl _) = p

Binary for Windows

Now we have coverage check!

Binary for Windows

Alow absurd patterns, e.g.

fun nomatchTest (n : N) (_: Id (succ (succ n)) (succ n)) : N where 
| n k !@ k

Binary for Windows

v0.1.1

update Example.shitt