Louis Warren louisswarren

Analyst, programmer, logician.

louisswarren / omega.agda

Last active September 20, 2018 21:07

Show there is no bijection from A to 2^A

	open import Agda.Builtin.Nat renaming (Nat to ℕ)
	open import Agda.Builtin.Equality
	open import Agda.Builtin.Sigma

	trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
	trans refl y = y

	data Bool : Set where
	False True : Bool

louisswarren / com.agda

Last active September 20, 2018 15:50

Commutativity of addition in Agda (for autumn school)

louisswarren / Fvec.agda

Created September 18, 2018 13:10

Functions from finite sets as a (terminating) alternative to vectors

	open import Agda.Builtin.Nat renaming (Nat to ℕ)
	open import Agda.Builtin.Equality

	data Vec (A : Set) : ℕ → Set where
	[] : Vec A zero
	_∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

	data Fin : ℕ → Set where
	fzero : ∀{n} → Fin (suc n)
	fsuc : ∀{n} → Fin n → Fin (suc n)

louisswarren / cite.agda

Created September 2, 2018 10:28

Stringify postulated objects

	open import Agda.Builtin.Nat renaming (Nat to ℕ)
	open import Agda.Builtin.String

	_>>_ = primStringAppend
	infixl 1 _>>_

	postulate ω : ℕ

	data Singular : ℕ → Set where
	singular : (n : ℕ) → Singular n

louisswarren / Decidable.agda

Last active December 4, 2018 01:58

Automata and finite types in agda

	module Decidable where

	open import Agda.Builtin.Equality public

	data ⊥ : Set where

	¬_ : (A : Set) → Set
	¬ A = A → ⊥

	⊥-elim : {A : Set} → ⊥ → A

louisswarren / Weich.agda

Created August 3, 2018 05:25

Give a proof or countermodel for the implicational fragment

	module Weich where

	open import Agda.Builtin.Bool
	open import Agda.Builtin.Equality

	open import Decidable
	open import List
	renaming (
	_∈_ to _[∈]_ ;
	_∉_ to _[∉]_ ;

louisswarren / closure.agda

Created August 1, 2018 02:33

Closure of a hierarchy in agda

	open import Decidable
	open import List

	data Arrow (A : Set) : Set where
	Atom : A → Arrow A
	_⇒_ : A → Arrow A → Arrow A

	data _⊢_ {A : Set} (αs : List (Arrow A)) : Arrow A → Set where
	triv : ∀{α} → α ∈ αs → αs ⊢ α
	elim : ∀{α β} → αs ⊢ (α ⇒ β) → αs ⊢ (Atom α) → αs ⊢ β

louisswarren / Declist.agda

Last active June 13, 2018 05:38

Searching with intensional equality, maybe

	open import Agda.Builtin.Bool
	open import Agda.Builtin.List
	open import Agda.Builtin.Equality

	-- See http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

	open import Search

	module Declist (A : Set)(_=dec=_ : BiDecidable _≡_) where

louisswarren / the.md

Created June 8, 2018 06:35

The programming language

The (θ\η)

Pronounced like theta, without the eta bit.

louisswarren / stringeq.agda

Created June 8, 2018 04:57

Is string equality even reflexive?

	open import Agda.Builtin.Bool
	open import Agda.Builtin.Equality
	open import Agda.Builtin.String

	data Inspect {A : Set}(x : A) : Set where
	_with≡_ : (y : A) → x ≡ y → Inspect x

	inspect : {A : Set} → (x : A) → Inspect x
	inspect x = x with≡ refl