This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data FakeChar = A | B | C | |
data ValidMyString : List Char -> Type where | |
VA : ValidMyString xs -> ValidMyString ('a' :: xs) | |
VB : ValidMyString xs -> ValidMyString ('b' :: xs) | |
VC : ValidMyString xs -> ValidMyString ('c' :: xs) | |
VNil : ValidMyString [] | |
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)} | |
-> List FakeChar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Mathematical Logic - Kleene | |
Basic Category Theory for Computer Scientists - Pierce | |
A Book of Abstract Algebra - Pinter | |
Conceptual Mathematics - Lawvere & Schanuel | |
An Introduction to Formal Logic - Smith | |
To Mock A Mockingbird - Smullyan | |
Introduction To Logic - Tarski | |
Purely Functional Data Structures - Okasaki | |
Topoi: The Categorial Analysis of Logic - Goldblatt | |
Lectures on the Curry-Howard Isomorphism - Sorensen, Urzyczyn |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Maths where | |
data Nat : Set where | |
zero : Nat | |
suc : Nat → Nat | |
plus : Nat → Nat → Nat | |
plus zero n = n | |
plus (suc m) n = suc (plus m n) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Routing where | |
open import Function hiding (type-signature) | |
open import Data.Bool hiding (_≟_) | |
open import Data.Maybe | |
open import Data.Char hiding (_≟_) | |
open import Data.String as String | |
open import Data.List as List hiding ([_]) | |
open import Data.Product hiding (curry; uncurry) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Categories.Agda.State where | |
open import Categories.Category | |
open import Categories.Agda | |
open import Categories.Agda.Product | |
open import Categories.Functor hiding (_≡_) | |
open import Categories.Functor.Product | |
open import Categories.Functor.Hom | |
open import Categories.Monad | |
open import Categories.Adjunction |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | |
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. | |
-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DeriveDataTypeable , Rank2Types , ViewPatterns #-} | |
import Control.Applicative | |
import Control.Arrow | |
import Control.Monad.Reader | |
import Control.Monad.Writer | |
import Data.Generics | |
import Data.Set (Set) | |
import qualified Data.Set | |
---------------------------------------------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Hello, my name ist {{name}} and I am {{age}} years old. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* It is not possible in Standard ML to construct an identity type (or any other | |
* indexed type), but that does not stop us from speculating. We can specify with | |
* a signature equality should mean, and then use a functor to say, "If there | |
* were a such thing as equality, then we could prove these things with it." | |
* Likewise, we can use the same trick to define the booleans and their | |
* induction principle at the type-level, and speculate what proofs we could | |
* make if we indeed had the booleans and their induction principle. | |
* | |
* Functions may be defined by asserting their inputs and outputs as | |
* propositional equalities in a signature; these "functions" do not compute, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 ) |
OlderNewer