Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid
Last active August 29, 2015 13:57
Show Gist options
  • Save larrytheliquid/9798857 to your computer and use it in GitHub Desktop.
Save larrytheliquid/9798857 to your computer and use it in GitHub Desktop.
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 : ℕ) : Set ℓ where
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
Foo.
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment