MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "implicitSizeVarUsedExplicitely.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.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  leq : Nat -> Nat -> Bool
{}
term  plus : .[A : Set] -> A -> A -> A
{}
type  List : + Size -> Set
term  List.nil : .[s!ze : Size] -> .[i < s!ze] -> List s!ze
term  List.nil : .[i : Size] -> < List.nil i : List $i >
term  List.cons : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat -> ^ List i -> List s!ze
term  List.cons : .[i : Size] -> ^(y1 : Nat) -> ^(y2 : List i) -> < List.cons i y1 y2 : List $i >
term  filter : .[i : Size] -> List i -> List i
{ filter [.$i] (List.nil [i]) = List.nil [i]
; filter [.$i] (List.cons [i] n l) = plus [List $i] (filter [i] l) (List.cons [i] n (filter [i] l))
}
term  quicksort : .[i : Size] -> List i -> List #
{ quicksort [.$i] (List.nil [i]) = List.nil [#]
; quicksort [.$i] (List.cons [i] n l) = plus [List #] (quicksort [i] (filter [i] l)) (List.cons [#] n (quicksort [i] (filter [i] l)))
}
type  Id : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a a >
--- evaluating ---
--- closing "implicitSizeVarUsedExplicitely.ma" ---