Skip to content

Instantly share code, notes, and snippets.



Last active Aug 29, 2015
What would you like to do?
Positivity checker
module Foo where
open import Level using ( Lift )
data : Set where
zero :
suc :
elimℕ : {ℓ} (P : Set ℓ)
(pzero : P zero)
(psuc : (n : ℕ) P n P (suc n))
(n : ℕ) P n
elimℕ P pzero psuc zero = pzero
elimℕ P pzero psuc (suc n) = psuc n (elimℕ P pzero psuc n)
ℕ∨Xpred₁ : {ℓ} (X : Set ℓ) (n : ℕ) Set
ℕ∨Xpred₁ X zero = Lift ℕ
ℕ∨Xpred₁ X (suc n) = X n
ℕ∨Xpred₂ : {ℓ} (X : Set ℓ) (n : ℕ) Set
ℕ∨Xpred₂ {ℓ = ℓ} X = elimℕ (λ _ Set ℓ) (Lift ℕ) (λ (m : ℕ) (ih : Set ℓ) X m)
data Foo {ℓ} (n : ℕ) : Setwhere
foo₁ : ℕ∨Xpred₁ Foo n Foo n
foo₂ : ℕ∨Xpred₂ Foo n Foo n
-- elimℕ (λ _ → Set ℓ) (Lift ℕ) (λ m ih → Foo m) n → Foo n
Foo is not strictly positive, because it occurs in the 4th argument
to elimℕ in the type of the constructor foo₂ in the definition of
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment