Skip to content

Instantly share code, notes, and snippets.

@mietek
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
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)
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
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
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
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)
(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)
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 / magic.erl
Created July 16, 2019 10:53
Erlang is magic!
-module(magic).
-export([loop/0, start/0]).
loop() ->
receive
Fun ->
Fun(),
loop()
end.
@mietek
mietek / keybase.md
Created July 12, 2019 16:46
Keybase proof

Keybase proof

I hereby claim:

  • I am mietek on github.
  • I am mietek (https://keybase.io/mietek) on keybase.
  • I have a public key ASC7JOFEAXt8XpqQVAUKRgl6x8YnzqyEnigshYRK-_71XQo

To claim this, I am signing this object: