class FunctionType:
def __init__(self, tyA, tyB):
self.tyA = tyA
self.tyB = tyB
def __eq__(self, other):
return self.tyA == other.tyA and self.tyB == other.tyB
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
{-# OPTIONS --postfix-projections #-} | |
module Choices where | |
open import Level using (0ℓ) renaming (suc to lsuc) | |
open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂) | |
open import Data.Bool using (true; false; if_then_else_; _∧_; not) | |
renaming (Bool to 𝔹) | |
open import Data.Nat using (ℕ; zero; suc; _≤ᵇ_) | |
open import Data.Unit using (⊤; tt) | |
open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
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
{-# OPTIONS --postfix-projections #-} | |
module tuple where | |
------------------------------------------------------------------------------ | |
-- |
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 localdefs where | |
mutual | |
data ty-ctx : Set where | |
ε : ty-ctx | |
_,-_ : (Δ : ty-ctx) → defn Δ → ty-ctx | |
data defn : ty-ctx → Set where | |
synonym : ∀ {Δ} → ty Δ → defn Δ | |
newtype : ∀ {Δ} → ty Δ → defn Δ |
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
{-# OPTIONS --prop --rewriting --confluence-check #-} | |
module param-rewrites where | |
open import Agda.Builtin.Unit | |
------------------------------------------------------------------------------ | |
-- Equality as a proposition | |
data _≡_ {a} {A : Set a} : A → A → Prop where | |
refl : ∀{a} → a ≡ a |
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
{-# OPTIONS --rewriting #-} | |
module cont-cwf where | |
open import Agda.Builtin.Sigma | |
open import Agda.Builtin.Unit | |
open import Agda.Builtin.Bool | |
open import Agda.Builtin.Nat | |
open import Data.Empty | |
import Relation.Binary.PropositionalEquality as Eq |
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
Require Import List. | |
Require Import FunctionalExtensionality. | |
Require Import ZArith. | |
Require Import Zcompare. | |
(* c.f. https://twitter.com/Hillelogram/status/987432184217731073 *) | |
Set Implicit Arguments. | |
Lemma map_combine : forall A B C (f : A -> B) (g : A -> C) xs, |
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
(* This is a demonstration of the use of the SML module system to | |
encode (Generalized Algebraic Datatypes) GADTs via Church | |
encodings. The basic idea is to use the Church encoding of GADTs in | |
System Fomega and translate the System Fomega type into the module | |
system. As I demonstrate below, this allows things like the | |
singleton type of booleans, and the equality type, to be | |
represented. | |
This was inspired by Jon Sterling's blog post about encoding proofs | |
in the SML module system: |