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:
(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 |
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 |
-- 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′ |
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 |
-module(magic). | |
-export([loop/0, start/0]). | |
loop() -> | |
receive | |
Fun -> | |
Fun(), | |
loop() | |
end. |
I hereby claim:
To claim this, I am signing this object: