Skip to content

Instantly share code, notes, and snippets.


Larry Diehl larrytheliquid

View GitHub Profile
View InferredPropositionalDescEliminatorConcat.agda
λ A m n →
(`Arg (Tag ("nil" ∷ "cons" ∷ []))
(λ t →
(λ _ →
(`Arg (Tag ("zero" ∷ "suc" ∷ []))
(λ t₁ → case (λ _ → Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
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 ∙ ε ∶ ℕ ⟩)
larrytheliquid / HypotheticalFunMatching.agda
Created Jun 29, 2013
What goes wrong if you were to allow matching against value/neutral forms of functions? Are there any good references on this?
View HypotheticalFunMatching.agda
open import Data.Bool
open import Data.Nat
module HypotheticalFunMatching where
Imagine that the expressions in the pattern positions are first evaluated to values/neutrals.
So for example, "not" really becomes elimBool and "_+_" becomes two nested elimℕ's.
A wildcard match is always necessary because there are infinitely many intentionally different
larrytheliquid / LocalProps.agda
Last active Dec 15, 2015
How does local completeness generalize to eliminators?
View LocalProps.agda
How does local completeness ( generalize to eliminators?
Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
View gist:5061869
airtheliquid:spire larrytheliquid$ ./spire
Enter type:
If (Not (Not True)) Bool Unit
Enter term:
Not True
Well typed!
=> False : Bool
View CrazyNames.agda
open import Data.Bool
open import Data.Nat
open import Data.String
module CrazyNames where
data U : Set where
`Bool `ℕ : U
El : U Set
El `Bool = Bool
View TrailEquality.agda
module TrailEquality where
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
data Maybe (A : Set) : Set where
just : (x : A) Maybe A
nothing : Maybe A
data : Set where
zero :
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 )
larrytheliquid / gist:3890780
Created Oct 15, 2012
IR DT Types + Terms
View gist:3890780
open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )
data ⊥ {a} : Set a where
! : ∀ {a b} {A : Set a} → ⊥ {b} → A
! ()
record ⊤ {a} : Set a where
constructor tt
larrytheliquid / gist:3889346
Created Oct 14, 2012
inductive-recursive universe for dependent types (no unicode)
View gist:3889346
module IRDTT where
open import Level
open import Data.Product using ( _,_ )
renaming ( Σ to Sigma ; proj₁ to proj1 ; proj₂ to proj2 )
open import Data.Sum
renaming ( __ to Sum ; inj₁ to inj1 ; inj₂ to inj2 )
record Unit {a} : Set a where
constructor tt
You can’t perform that action at this time.