MiniAgda by Andreas Abel and Karl Mehltretter --- opening "nat.ma" --- --- scope checking --- --- type checking --- type SNat : + Size -> Set term SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze term SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i > term SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze term SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i > term add : SNat # -> SNat # -> SNat # { add (SNat.zero [.#]) y = y ; add (SNat.succ [.#] x) y = SNat.succ [#] (add x y) } term inc : .[i : Size] -> .[j : Size] -> SNat i -> SNat $i { inc [i] [j] x = SNat.succ [i] x } term minus : .[i : Size] -> SNat i -> SNat # -> SNat i { minus [i] (SNat.zero [j < i]) y = SNat.zero [j] ; minus [i] x (SNat.zero [.#]) = x ; minus [i] (SNat.succ [j < i] x) (SNat.succ [.#] y) = minus [j] x y } term test : SNat # term test = minus [#] (SNat.succ [#] (SNat.succ [#] (SNat.zero [#]))) (SNat.succ [#] (SNat.zero [#])) term div : .[i : Size] -> SNat i -> SNat # -> SNat i { div [i] (SNat.zero [j < i]) y = SNat.zero [j] ; div [i] (SNat.succ [j < i] x) y = SNat.succ [j] (div [j] (minus [j] x y) y) } type Bool : Set term Bool.tt : < Bool.tt : Bool > term Bool.ff : < Bool.ff : Bool > term true : .[i : Size] -> SNat i -> Bool { true [.$i] (SNat.zero [i]) = Bool.tt ; true [.$i] (SNat.succ [i] x) = true [i] x } term ok : .[Size] -> Bool { ok [i] = Bool.tt } --- evaluating --- test has whnf (minus # (succ # (succ # (zero #))) (succ # (zero #))) test evaluates to minus # (succ # (succ # (zero #))) (succ # (zero #)) --- closing "nat.ma" ---