{{ message }}

Instantly share code, notes, and snippets.

# G. Allais gallais

Created Aug 2, 2020
Returning a smaller sized list
View Smaller.agda
 open import Agda.Builtin.Size open import Data.Maybe.Base data List {n} (T : Set n) (i : Size) : Set n where [] : List T i _∷_ : ∀ {j : Size< i} → T → List T j → List T i data Smaller {n} (T : Size → Set n) (i : Size) : Set n where [_] : {j : Size< i} → T j → Smaller T i
Last active Jun 22, 2020
View SyntaxDesc.agda
 {-# OPTIONS --safe --without-K #-} module SyntaxDesc (I : Set) where open import Agda.Primitive using () renaming (Set to Type) open import Data.Nat.Base open import Data.Fin.Base open import Data.List.Base using (List; []; _∷_; _++_) data Desc : Type₀ where
Created May 22, 2020
Palindrome via an accumulator-based definition.
View PalAcc.v
 Require Import List. Inductive PalAcc {A : Type} (acc : list A) : list A -> Type := Even : PalAcc acc acc | Odd : forall x, PalAcc acc (x :: acc) | Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs) . Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs.
Last active Mar 4, 2020
Terminating map via commuting conversions
View get.v
 Inductive Tree (A : Set) : Set := | Leaf : A -> Tree A | Node : bool -> Tree A * Tree A -> Tree A. Definition subTree {A : Set} (b : bool) (lr : Tree A * Tree A) : Tree A := match (b, lr) with | (true, (a, b)) => a | (false, (a, b)) => b end.
Created Mar 2, 2020
Using the lack of strict positivity to run an infinite computation
View Negative.idr
 data EventT : (event : Type) -> (m : Type -> Type) -> (a : Type) -> Type where MkEventTCont : (event -> m (EventT event m a)) -> EventT event m a MkEventTTerm : m a -> EventT event m a MkEventTEmpty : EventT event m a data LAM : (x : Type) -> Type where App : x -> x -> LAM x Lam : (x -> x) -> LAM x LC : Type
Created Dec 17, 2019
example of search
View search.agda
 open import Agda.Builtin.Equality open import Agda.Builtin.Nat hiding (_+_; _<_) open import Data.Nat open import Data.Nat.Properties open import Relation.Binary -- C-c C-z RET _*_ _≡_ RET
Created Jun 4, 2019
Use case for ∷-dec
View Rose.agda
 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
Last active Mar 26, 2019
Raw linear terms
View linear.agda
 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
Created Mar 26, 2019
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
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