Skip to content

Instantly share code, notes, and snippets.

@louisswarren
Forked from milesrout/meme.agda
Last active Mar 21, 2019
Embed
What would you like to do?
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
_ : 044
_ = m≤⊔n≡n
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment