mietek

module Prime where

open import Codata.Musical.Notation
  using (∞ ; ♯_ ; ♭)

open import Codata.Musical.Stream
  using (_∷_ ; Stream)

open import Data.Empty
  using (⊥ ; ⊥-elim)

mietek

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

-- 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

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

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

(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

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

-module(magic).
-export([loop/0, start/0]).

loop() ->
  receive
    Fun ->
      Fun(),
      loop()
  end.

mietek

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:

mietek

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