Skip to content

Instantly share code, notes, and snippets.

View mietek's full-sized avatar

Miëtek Bak mietek

282 followers · 0 following
View GitHub Profile
@mietek
mietek / Prime.agda
Last active December 25, 2023 22:08 — forked from copumpkin/Prime.agda
There are infinite primes
module Prime where
open import Codata.Musical.Notation
using (∞ ; ♯_ ; ♭)
open import Codata.Musical.Stream
using (_∷_ ; Stream)
open import Data.Empty
using (⊥ ; ⊥-elim)
@mietek
mietek / Choose.agda
Last active August 15, 2020 03:35 — forked from davidad/0_0_1.v
There is exactly one way to choose 0 elements from the empty set.
module Choose where
open import Data.Product using (_,_ ; proj₁ ; proj₂ ; ∃) renaming (_×_ to _∧_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; sym ; subst)
open import Relation.Nullary using (¬_)
infix 0 _⇔_
_⇔_ : Set → Set → Set
A ⇔ B = (A → B) ∧ (B → A)
@mietek
mietek / lisp15.lisp
Created June 17, 2020 14:39 — forked from bitmappergit/lisp15.lisp
(defun lapply (fn x a)
(cond ((atom fn) (cond ((eq fn 'car) (caar x))
((eq fn 'cdr) (cdar x))
((eq fn 'cons) (cons (car x) (cadr x)))
((eq fn 'atom) (atom (car x)))
((eq fn 'eq) (eq (car x) (cadr x)))
((eq fn 'read) (read))
(t (lapply (leval fn a) x a))))
((eq (car fn) 'lambda) (leval (caddr fn) (pairlis (cadr fn) x a)))
((eq (car fn) 'label) (lapply (caddr fn) (cons (cons (cadr fn)
@mietek
mietek / Irrelevance-Issue.agda
Last active August 13, 2019 23:43 — forked from EdNutting/Irrelevance-Issue.agda
open import Data.Nat as Nat
module Irrelevance-Issue (someMax₁ : ℕ) where
open import Level using () renaming ( _⊔_ to _⊔ₗ_)
open import Function
open import Data.Fin as Fin renaming (_≟_ to _≟f_)
hiding (_<_; _≤_; _+_)
open import Data.Product as Product
@mietek
mietek / SystemF.agda
Last active June 30, 2019 21:41 — forked from AndrasKovacs/SystemF.agda
Embedding of predicative polymorphic System F in Agda.
open import Function
open import Data.Nat
open import Data.Fin renaming (_+_ to _f+_)
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Vec
open import Data.Vec.Properties
@mietek
mietek / Category.agda
Last active May 31, 2019 01:44 — forked from dorchard/Category.agda
Definition of a category as an Agda record: level polymorphic in the objects and arrows
module Category where
open import Agda.Primitive public
using (Level ; _⊔_ ; lzero ; lsuc)
open import Agda.Builtin.Equality public
using (_≡_ ; refl)
record Category ℓ ℓ′ : Set (lsuc (ℓ ⊔ ℓ′)) where
@mietek
mietek / Main.agda
Created July 30, 2017 01:59 — forked from gelisam/Main.agda
cat in Agda using copatterns
{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).
open import Data.Nat
open import Data.Unit
open import Data.Bool
open import Data.Char
@mietek
mietek / Main.agda
Created July 30, 2017 01:59 — forked from puffnfresh/Main.agda
cat in Agda
module Main where
import IO.Primitive as Prim
open import Coinduction
open import Data.Unit
open import IO
cat : IO ⊤
cat = ♯ getContents >>= (\cs → ♯ (putStr∞ cs))
@mietek
mietek / AnIntro.md
Last active August 29, 2015 14:09 — forked from chrisdone/AnIntro.md

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions: