Scott Fleischman scott-fleischman

Apollonius Rhodius

Thucydides

Charles Morris 1891
- Book 1 https://books.google.com/books?id=xSkBAAAAYAAJ
Loeb, William Heinemann, 1920
- Volume 2, Books III, IV https://books.google.com/books?id=ZBsMAAAAIAAJ
Charles Forster Smith, 1921

	module AgdaFromNothing where

	data Bool : Set where
	true : Bool
	false : Bool

	not : Bool -> Bool
	not true = false
	not false = true

	module _ where

	-- from McBride (2014) How to Keep Your Neighbours in Order

	data 𝟘 : Set where
	record 𝟙 : Set where
	constructor <>

	record Σ (A : Set) (B : A → Set) : Set where
	constructor _,_

	module _ where

	open import Agda.Builtin.List

	infixl 6 _++_
	_++_ : {A : Set} → (xs ys : List A) → List A
	[] ++ ys = ys
	(x ∷ xs) ++ ys = x ∷ xs ++ ys

	infixr 6 _+_

	module RecordEta where

	open import Agda.Builtin.Equality

	module Eta where
	record Pair (A B : Set) : Set where
	constructor pair
	field
	fst : A
	snd : B

	module _ where

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

	id1 : (f : Bool → Bool) → f ≡ f
	id1 f = refl

	f : Bool → Bool
	f true = false

	module _ where

	open import Agda.Builtin.Equality
	data ⊥ : Set where

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

	data A : Set where
	a1 a2 a3 : A

	{-# OPTIONS --exact-split #-}

	module Neighbor where

	data 𝟘 : Set where
	open import Agda.Builtin.Unit renaming (⊤ to 𝟙)

	infixr 5 _×_ _,_
	record Sg (A : Set) (B : A → Set) : Set where
	constructor _,_

	module List where

	open import Agda.Builtin.List
	open import Agda.Builtin.Nat

	data ListLength (A : Set) : Nat → Set where
	[] : ListLength A zero
	_∷_ : (x : A) → {n : Nat} → (xs : ListLength A n) → ListLength A (suc n)

	data Fin : Nat → Set where