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

mietek

module Proset where

open import Agda.Primitive public
  using (_⊔_)

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


--------------------------------------------------------------------------------

mietek

module Category where

open import Agda.Primitive public
  using (Level ; _⊔_)
  renaming (lzero to ℓ₀)

open import Function public
  using (id ; flip)
  renaming (_∘′_ to _∘_)

mietek

module EncodeDecode where

open import Agda.Builtin.Char
  using (Char)
  renaming ( primCharToNat to ord
           ; primNatToChar to chr
           )

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

mietek

module STLCSemantics where


--------------------------------------------------------------------------------


-- Types
infixr 7 _⇒_
data Type : Set
  where