mietek’s gists

mietek / mi.el

Last active June 22, 2024 22:22

My color scheme for emacs-agda-mode

	(eval-after-load "agda2-mode" '(progn
	(face-spec-set 'font-lock-comment-face '((((background light)) (:foreground "#999999")) (((background dark)) (:foreground "#666666"))) 'face-defface-spec)
	(face-spec-set 'agda2-highlight-keyword-face '((((background light)) (:foreground "#666666")) (((background dark)) (:foreground "#999999"))) 'face-defface-spec)
	(face-spec-set 'agda2-highlight-markup-face '((((background light)) (:foreground "#666666")) (((background dark)) (:foreground "#999999"))) 'face-defface-spec)
	(face-spec-set 'agda2-highlight-operator-face '((((background light)) (:foreground "#666666")) (((background dark)) (:foreground "#999999"))) 'face-defface-spec)
	(face-spec-set 'agda2-highlight-pragma-face '((((background light)) (:foreground "#666666")) (((background dark)) (:foreground "#999999"))) 'face-defface-spec)
	(face-spec-set 'agda2-highlight-primitive-type-face '((((background light)) (:fo

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 / gist:efd4b24ab30f2d600de79b9ea27efc5b

Created December 23, 2023 17:06

Oat cookies

	OAT COOKIES v1.0

	rehydrate 1 cup raisins
	melt 1/2 pack salted butter
	prepare large mixing bowl

	add 2 cups white sugar
	add 1 table spoon ground cinnamon
	add 1/2 cup whole milk
	add 1/2 pack melted salted butter

mietek / Sigma.agda

Last active September 20, 2021 19:21

	-- To simplify defining ChurchSigma.
	{-# OPTIONS --type-in-type #-}

	module Sigma where

	open import Axiom.Extensionality.Propositional using (Extensionality)
	open import Level using (_⊔_)
	open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; module ≡-Reasoning)
	open ≡-Reasoning

mietek / Cong.agda

Last active July 17, 2021 10:10

	open import Agda.Builtin.Equality using (_≡_ ; refl)

	infixl 9 _&_
	_&_ : ∀ {a b} {A : Set a} {B : Set b}
	(f : A → B) {x x′} → x ≡ x′ → f x ≡ f x′
	f & refl = refl

	infixl 8 _⊗_
	_⊗_ : ∀ {a b} {A : Set a} {B : Set b} {f f′ : A → B} {x x′} →
	f ≡ f′ → x ≡ x′ → f x ≡ f′ x′

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 / magic.erl

Created July 16, 2019 10:53

Erlang is magic!

mietek / keybase.md

Created July 12, 2019 16:46

Keybase proof

I hereby claim:

To claim this, I am signing this object:

Miëtek Bak mietek