{{ message }}

Instantly share code, notes, and snippets.

# Larry Diehllarrytheliquid

Last active Jan 3, 2016
Canonical terms for the concat function in this blog post: http://spire-lang.org/blog/2014/01/15/modeling-elimination-of-described-types/
View InferredPropositionalDescEliminatorConcat.agda
 λ A m n → ind (`Arg (Tag ("nil" ∷ "cons" ∷ [])) (λ t → case (λ _ → Desc (μ (`Arg (Tag ("zero" ∷ "suc" ∷ [])) (λ t₁ → case (λ _ → Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))
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 ∙ ε ∶ ℕ ⟩)
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 functions.
Last active Dec 15, 2015
How does local completeness generalize to eliminators?
View LocalProps.agda
 {- How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) 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. Caveats: 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. -}
Created Mar 1, 2013
View gist:5061869
 airtheliquid:spire larrytheliquid\$ ./spire Enter type: If (Not (Not True)) Bool Unit Enter term: Not True Well typed! => False : Bool
Last active Dec 12, 2015
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
Created Feb 3, 2013
Trail equality
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 : ℕ
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 )
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
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.