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 Data.List using (List); open List | |
open import Data.List.Properties | |
open import Data.Product | |
open import Relation.Nullary | |
open import Relation.Nullary.Decidable | |
open import Relation.Nullary.Product | |
open import Relation.Binary | |
open import Relation.Binary.PropositionalEquality | |
private variable A : Set |
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 Data.Nat.Base | |
open import Data.Vec | |
open import Data.Bool.Base using (Bool; false; true) | |
open import Data.Product | |
variable | |
m n : ℕ | |
b : Bool | |
Γ Δ Ξ T I O : Vec Bool 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
open import Size | |
open import Codata.Thunk | |
data BinaryTreePath (i : Size) : Set where | |
here : BinaryTreePath i | |
branchL : Thunk BinaryTreePath i → BinaryTreePath i | |
branchR : Thunk BinaryTreePath i → BinaryTreePath i | |
zero : ∀ {i} → BinaryTreePath i | |
zero = branchL λ where .force → zero |
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
module scope where | |
import Level as L | |
open import Data.Nat.Base | |
open import Data.Vec hiding (_>>=_) | |
open import Data.Fin.Base | |
open import Data.String | |
open import Data.Maybe as Maybe | |
open import Data.Product as Prod | |
open import Relation.Nullary |
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 Level | |
open import Data.List.Base hiding (filter) | |
open import Data.List.Relation.Unary.All | |
open import Data.List.Relation.Ternary.Interleaving.Propositional | |
open import Function | |
open import Relation.Nullary | |
open import Relation.Unary | |
module _ {a} {A : Set a} where |
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 Relation.Nullary | |
open import Agda.Builtin.Equality | |
data X : Set where | |
a b c : X | |
firstA : (x y z : X) → X | |
firstA a y z = a | |
firstA x a z = a | |
firstA x y a = a |
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
module Container | |
%default total | |
record Container where | |
constructor MkContainer | |
shape : Type | |
position : shape -> Type | |
container : Container -> Type -> Type |
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 Relation.Binary | |
module Reasoning {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} | |
{_≈_ : Rel A ℓ₁} (≈-trans : Transitive _≈_) (≈-sym : Symmetric _≈_) (≈-refl : Reflexive _≈_) | |
{_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-respʳ-≈ : _≤_ Respectsʳ _≈_) (≤-refl : Reflexive _≤_) | |
{_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<-respʳ-≈ : _<_ Respectsʳ _≈_) (<⇒≤ : _<_ ⇒ _≤_) | |
(<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z) | |
(≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z) | |
where |
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
module bins where | |
open import Size | |
open import Codata.Stream | |
open import Codata.Thunk | |
open import Data.List.Base as List using (List; _∷_; []) | |
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; [_]) | |
open import Function | |
open import Relation.Unary |
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 Relation.Binary.PropositionalEquality | |
open import Relation.Binary.HeterogeneousEquality | |
open import Data.Maybe | |
open import Function | |
cong⁻¹ : ∀ {A B : Set} {a a'} (f : A → Maybe B) → | |
(eq : a ≡ a') → | |
from-just (f a) ≅ from-just (f a') | |
cong⁻¹ {a = a} f refl = refl |