MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MuOnlyPosNotSPos.ma" --- --- scope checking --- --- type checking --- type Mu : ++(F : + Set -> Set) -> Set error during typechecking: Mu /// constructor Mu.inn /// new Mu : (++(F : (+Set -> Set)::Set) -> Set) /// new F : (+Set -> {Set {Mu = (v0 Up (++(F : (+Set -> Set)::Set) -> Set))}}) /// inferExpr' ^ F (Mu F) -> Mu F /// inferExpr' F (Mu F) /// checkApp (+Set -> {Set {Mu = (v0 Up (++(F : (+Set -> Set)::Set) -> Set))}}) eliminated by Mu F /// inferExpr' Mu F /// checkApp (++(F : (+Set -> Set)::Set) -> Set) eliminated by F /// inferExpr' F /// inferExpr: variable F : + Set -> Set may not occur /// , because of polarity /// polarity check ++ <= + failed