MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "dataNotMonotone.ma" ---
--- scope checking ---
--- type checking ---
type  Stream : ^(A : Set) -> - Size -> Set
term  Stream.consStream : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : Stream A i) -> < Stream.consStream i y1 y2 : Stream A $i >
type  NotMon : ^(A : Set) -> + Size -> Set
error during typechecking:
NotMon
/// constructor NotMon.consBla
/// szConstructor NotMon : .[A : Set] -> .[i : Size] -> ^(y1 : Stream A i) -> ^(y2 : NotMon A i) -> < NotMon.consBla i y1 y2 : NotMon A $i >
/// new A : Set
/// new i <= #
/// szSizeVarUsage of i in ^(y1 : Stream A i) -> ^(y2 : NotMon A i) -> < NotMon.consBla i y1 y2 : NotMon A $i >
/// checking Stream A i  to be isotone in variable i
/// leqVal'  Stream A i  <=+  Stream A $i : Set #
/// leqVal'  i  <=-  $i : Size
/// leSize i <=- $i
/// leSize' $i <= i
/// leSize: 0 + 1 <= 0 failed