Skip to content

Instantly share code, notes, and snippets.

Larry Diehl larrytheliquid

Block or report user

Report or block larrytheliquid

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
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
----------------------------------------------------------------------
@larrytheliquid
larrytheliquid / LabelledAdd1.agda
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…
View LabelledAdd1.agda
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 ∙ ε ∶ ℕ ⟩)
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
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
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)
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
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".
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
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
@larrytheliquid
larrytheliquid / gist:3909860
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.