Skip to content

Instantly share code, notes, and snippets.

View choice.agda
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
@gallais
gallais / scopecheck.agda
Created Mar 19, 2019
Crash course in scope checking
View scopecheck.agda
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
@gallais
gallais / filter.agda
Created Mar 3, 2019
Fully certified filter
View filter.agda
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
@gallais
gallais / ViewExample.agda
Last active Feb 13, 2019
Using a View makes proving easier
View ViewExample.agda
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
View Container.idr
module Container
%default total
record Container where
constructor MkContainer
shape : Type
position : shape -> Type
container : Container -> Type -> Type
View Reasoning.agda
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
View bins.agda
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
@gallais
gallais / generic-injective.agda
Created Sep 29, 2018
Generic combinator for injectivity proofs.
View generic-injective.agda
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
@gallais
gallais / atleastn.agda
Last active Sep 15, 2018
lists of size at least n
View atleastn.agda
open import Data.Nat
module atleastn (n : ℕ) {a} (A : Set a) where
open import Data.List using (List; length)
open import Data.Vec
record SizedList : Set a where
field list : List A
size : length list ≥ n
@gallais
gallais / Names.agda
Created Jun 2, 2018
Names with offsets
View Names.agda
open import Data.String.Base
open import Data.Nat.Base
open import Data.List.Base
open import Relation.Binary.PropositionalEquality
infix 5 _at_
record Variable : Set where
constructor _at_
field name : String