Skip to content

Instantly share code, notes, and snippets.

# louisswarren/implicit.agda

Forked from milesrout/meme.agda
Last active Mar 21, 2019
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 open import Agda.Builtin.Bool data ⊥ : Set where record ⊤ : Set where isTrue : Bool → Set isTrue true = ⊤ isTrue false = ⊥ data ℕ : Set where zero : ℕ suc : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} variable n m p : ℕ _≤_ : ℕ → ℕ → Bool zero ≤ m = true suc n ≤ zero = false suc n ≤ suc m = n ≤ m data _⊔_≡_ : ℕ → ℕ → ℕ → Set where m≥⊔n≡m : {_ : isTrue (n ≤ m)} --------- → m ⊔ n ≡ m m≤⊔n≡n : {_ : isTrue (m ≤ n)} --------- → m ⊔ n ≡ n _ : 0 ⊔ 4 ≡ 4 _ = m≤⊔n≡n
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 data ℕ : Set where zero : ℕ suc : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} variable n m p : ℕ data _≤_ : ℕ → ℕ → Set where z≤n : zero ≤ n s≤s : m ≤ n ------------- → suc m ≤ suc n data _⊔_≡_ : ℕ → ℕ → ℕ → Set where m≥⊔n≡m : n ≤ m --------- → m ⊔ n ≡ m m≤⊔n≡n : m ≤ n --------- → m ⊔ n ≡ n infix 4 _≤_ data Formula : ℕ → Set where var : (n : ℕ) → n ≤ m → Formula m ∩_ : Formula m → Formula (suc m) ∪_ : Formula m → Formula (suc m) α : Formula m → Formula n → (m ⊔ n ≡ p) → Formula p ν : Formula m → Formula n → (m ⊔ n ≡ p) → Formula p x : Formula zero x = var zero z≤n ∩xx : Formula (suc zero) ∩xx = ∩ (var zero z≤n) xα∩xx : Formula (suc zero) xα∩xx = α x ∩xx (m≤⊔n≡n z≤n) ∩xxαx : Formula (suc zero) ∩xxαx = α ∩xx x (m≥⊔n≡m z≤n) ∩xxα∩xx : Formula (suc zero) ∩xxα∩xx = α ∩xx ∩xx (m≥⊔n≡m (s≤s z≤n))
to join this conversation on GitHub. Already have an account? Sign in to comment