abella-prover/abella — pull request #28 by chaudhuri (2014-10-02 14:22:12+00:00)
Title: Extend the stratification checker to complain about higher-order arguments

The following definitions now cause warnings:

Define bad : prop -> prop by
bad P := bad P -> false.

Define ugly : prop by
ugly := (ugly -> false) -> false.

Define not : prop -> prop by
not P := P -> false.

Define r1 : prop -> prop by
r1 P := P. /* no warning here */

Define r2 : prop -> prop by
r2 P := r1 P -> false.

The compile-time flag `Abella.stratification_warnings_are_errors` can be used to turn stratification warnings into errors. Currently this is set to `false` for backwards compatibility.