Skip to content

Instantly share code, notes, and snippets.

@gallais
gallais / ElemSplit.idr
Created Sep 30, 2021
Magic pattern-matching on `Elem`
View ElemSplit.idr
import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality
%default total
toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2
@gallais
gallais / Smaller.agda
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
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
@gallais
gallais / PalAcc.v
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.
@gallais
gallais / get.v
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.
@gallais
gallais / Negative.idr
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
@gallais
gallais / search.agda
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
@gallais
gallais / Rose.agda
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
@gallais
gallais / linear.agda
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
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