MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "list.ma" ---
--- scope checking ---
--- type checking ---
type  List : ^(A : Set) -> Set
term  List.nil : .[A : Set] -> < List.nil : List A >
term  List.cons : .[A : Set] -> ^(y0 : A) -> ^(y1 : List A) -> < List.cons y0 y1 : List A >
--- evaluating ---
--- closing "list.ma" ---