mietek’s gists

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 / 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 / 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 / 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 / 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 / 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 / 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 / Main.agda

Created July 30, 2017 01:59 — forked from puffnfresh/Main.agda

cat in Agda

mietek / AnIntro.md

Last active August 29, 2015 14:09 — forked from chrisdone/AnIntro.md

Basic unit type:

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

Basic functions:

Miëtek Bak mietek