MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "Fib2.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 >
type  Nat : Set
type  Nat = SNat #
term  add : Nat -> Nat -> Nat
{ add (SNat.zero [.#]) = \ y -> y
; add (SNat.succ [.#] x) = \ y -> SNat.succ [#] (add x y)
}
type  Stream : ++(A : Set) -> - Size -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(head : A) -> ^(tail : Stream A i) -> < Stream.cons i head tail : Stream A $i >
term  head : .[A : Set] -> .[i : Size] -> (cons : Stream A $i) -> A
{ head [A] [i] (Stream.cons [.i] #head #tail) = #head
}
term  tail : .[A : Set] -> .[i : Size] -> (cons : Stream A $i) -> Stream A i
{ tail [A] [i] (Stream.cons [.i] #head #tail) = #tail
}
term  zipWith : .[A : Set] -> .[B : Set] -> .[C : Set] -> (A -> B -> C) -> .[i : Size] -> Stream A i -> Stream B i -> Stream C i
{ zipWith [A] [B] [C] f $[i < #] (Stream.cons [.i] a as) (Stream.cons [.i] b bs) = Stream.cons [i] (f a b) (zipWith [A] [B] [C] f [i] as bs)
}
term  n0 : Nat
term  n0 = SNat.zero [#]
term  n1 : Nat
term  n1 = SNat.succ [#] n0
term  fib : .[i : Size] -> Stream Nat i
{ fib $[i < #] = Stream.cons [i] n0 (zipWith [Nat] [Nat] [Nat] add [i] (Stream.cons [i] n1 (fib [i])) (fib [i]))
}
term  fib2 : .[i : Size] -> Stream Nat (i + i)
error during typechecking:
fib2
/// clause 1
/// right hand side
/// checkExpr 1 |- cons (i + i) n0 (zipWith Nat Nat Nat add (i + i) (cons (i + i) n1 (fib2 i)) (fib2 i)) : Stream Nat ($i + $i)
/// checkForced fromList [(i,0)] |- cons (i + i) n0 (zipWith Nat Nat Nat add (i + i) (cons (i + i) n1 (fib2 i)) (fib2 i)) : Stream Nat ($i + $i)
/// leqVal' (subtyping)  < Stream.cons (i + i) (SNat.zero #) (zipWith Nat Nat Nat add (i + i) (Stream.cons [i + i] n1 (fib2 [i])) (fib2 [i])) : Stream Nat $(i + i) >  <=+  Stream Nat ($i + $i)
/// leqVal' (subtyping)  Stream Nat $(i + i)  <=+  Stream Nat ($i + $i)
/// leqVal'  $(i + i)  <=-  $$(i + i) : Size
/// leSize $(i + i) <=- $$(i + i)
/// leSize i + i <=- $(i + i)
/// leSize' $(i + i) <= i + i
/// leSize: 0 + 1 <= 0 failed