{{ message }}

Instantly share code, notes, and snippets.

# Larry Diehllarrytheliquid

Last active Jan 5, 2019
View FSM.agda
 module FSM where data Bool : Set where true false : Bool data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A ----------------------------------------------------------------------
Last active May 13, 2018
Labelled types demo ala "The view from the left" by McBride & McKinna. Labels are a cheap alternative to dependent pattern matching. You can program with eliminators but the type of your goal reflects the dependent pattern match equation that you would have done. Inductive hypotheses are also labeled, and hence you get more type safety from usin…
 open import Data.Nat open import Data.String open import Function open import LabelledTypes module LabelledAdd1 where ---------------------------------------------------------------------- add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩ add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)
Last active Oct 26, 2017
View Weed.agda
 module Weed where data ⊥ : Set where magic : {A : Set} → ⊥ → A magic () data Weed (A : Set) : Set where grow : (A → Weed A) → Weed A
Last active Feb 26, 2017
Generic representation: https://is.gd/rms0P7
View VecIR.agda
 open import Data.Nat open import Data.Product open import Data.String open import Relation.Binary.PropositionalEquality module _ where mutual data Vec₁ (A : Set) : Set where nil : Vec₁ A cons : (n : ℕ) → A → (xs : Vec₁ A) → Vec₂ xs ≡ n → Vec₁ A
Created Feb 10, 2017
View VecIIR.agda
 open import Data.Nat open import Data.Fin renaming ( zero to here ; suc to there ) open import Data.Product open import Relation.Binary.PropositionalEquality module _ where mutual data Vec₁ (A : Set) : ℕ → Set where nil₁ : Vec₁ A zero cons₁ : {n : ℕ} → A → (xs : Vec₁ A n) → toℕ (Vec₂ xs) ≡ n → Vec₁ A (suc n)
Created Feb 6, 2017
View General.agda
 open import Data.Unit open import Data.Bool open import Data.Nat open import Data.Product module _ where ---------------------------------------------------------------------- data Desc (I : Set) : Set₁ where `ι : I → Desc I
Last active Feb 5, 2017
Extension to IIR here https://gist.github.com/larrytheliquid/14bf1ce208c13e543a6d20f60e903ae9
View GenerallyIndexed.agda
 open import Data.Unit open import Data.Bool open import Data.Nat open import Data.Product module _ where {- This odd approach gives you 2 choices when defining an indexed type: 1. Use a McBride-Dagand encoding so your datatype "need not store its indices".
Last active Feb 5, 2017
Inductive-recursive and infinitary version of https://gist.github.com/larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c
View SafeGenerallyIndexedIR.agda
 open import Data.Unit open import Data.Product module _ where ---------------------------------------------------------------------- data Desc (I : Set) (O : I → Set) : Set₁ where `ι : (i : I) (o : O i) → Desc I O `δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O `σ : (A : Set) (D : A → Desc I O) → Desc I O
Created Jan 6, 2017
View CoList.agda
 {-# OPTIONS --copatterns #-} module CoList where {- High-level intuition: codata CoList (A : Set) : Set where nil : CoList A cons : A → CoList A → CoList A append : ∀{A} → CoList A → CoList A → CoList A
Last active Apr 28, 2016
inductive-recursive universe for dependent types
View gist:3909860
 open import Data.Empty using ( ⊥ ; ⊥-elim ) open import Data.Unit using ( ⊤ ; tt ) open import Data.Bool using ( Bool ; true ; false ; if_then_else_ ) renaming ( _≟_ to _≟B_ ) open import Data.Nat using ( ℕ ; zero ; suc ) renaming ( _≟_ to _≟ℕ_ ) open import Data.Product using ( Σ ; _,_ ) open import Relation.Nullary using ( Dec ; yes ; no ) open import Relation.Binary using ( Decidable ) open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
You can’t perform that action at this time.