MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DeepForcedConstructors.ma" --- --- scope checking --- --- type checking --- type Bool : Set term Bool.true : < Bool.true : Bool > term Bool.false : < Bool.false : Bool > term not : Bool -> Bool { not Bool.true = Bool.false ; not Bool.false = Bool.true } type Nat : ^ Bool -> Set term Nat.zero : < Nat.zero : Nat Bool.true > term Nat.succ : ^(b : Bool) -> ^(y1 : Nat b) -> < Nat.succ b y1 : Nat Bool.false > term f : (b : Bool) -> .[Nat b] -> Bool error during typechecking: f /// clause 2 /// pattern succ .true zero /// pattern zero /// checkPattern: constructor Nat.zero of non-computational argument zero : (Nat .Bool.true{}) not forced