MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MergeWith.ma" --- --- scope checking --- --- type checking --- type Bool : Set term Bool.true : < Bool.true : Bool > term Bool.false : < Bool.false : Bool > type Nat : Set term Nat.zero : < Nat.zero : Nat > term Nat.suc : ^(y0 : Nat) -> < Nat.suc y0 : Nat > type List : Set term List.nil : < List.nil : List > term List.cons : ^(y0 : Nat) -> ^(y1 : List) -> < List.cons y0 y1 : List > term leq : Nat -> Nat -> Bool {} term merge : List -> List -> List term merge_aux : Nat -> List -> List -> Nat -> List -> List -> Bool -> List { merge List.nil l = l ; merge l List.nil = l ; merge (List.cons x xs) (List.cons y ys) = merge_aux x xs (List.cons x xs) y ys (List.cons y ys) (leq x y) } { merge_aux x xs xxs y ys yys Bool.true = List.cons x (merge xs yys) ; merge_aux x xs xxs y ys yys Bool.false = List.cons y (merge xxs ys) } --- evaluating --- --- closing "MergeWith.ma" ---