MiniAgda by Andreas Abel and Karl Mehltretter --- opening "addWith.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 ote : .[i : Size] -> SNat i -> SNat i { ote [.$i] (SNat.zero [i]) = SNat.zero [i] ; ote [.$$i] (SNat.succ [.$i] (SNat.zero [i])) = SNat.zero [i] ; ote [.$$i] (SNat.succ [.$i] (SNat.succ [i] x)) = SNat.succ [$i] (SNat.succ [i] (ote [i] x)) } term addWith : (.[k : Size] -> SNat k -> SNat k) -> .[i : Size] -> .[j : Size] -> SNat i -> SNat j -> SNat # { addWith f [.$i] [j] (SNat.zero [i]) y = y ; addWith f [.$i] [j] (SNat.succ [i] x) y = SNat.succ [#] (addWith f [j] [i] (f [j] y) (f [i] x)) } term three : SNat # term three = SNat.succ [#] (SNat.succ [#] (SNat.succ [#] (SNat.zero [#]))) term four : SNat # term four = SNat.succ [#] three term bla : SNat # term bla = addWith ote [#] [#] four three --- evaluating --- bla has whnf SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.zero{i = #}}}} bla evaluates to SNat.succ # (SNat.succ # (SNat.succ # (SNat.zero #))) --- closing "addWith.ma" ---