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:
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:
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 |
module Proset where | |
open import Agda.Primitive public | |
using (_⊔_) | |
open import Agda.Builtin.Equality public | |
using (_≡_ ; refl) | |
-------------------------------------------------------------------------------- |
module Category where | |
open import Agda.Primitive public | |
using (Level ; _⊔_) | |
renaming (lzero to ℓ₀) | |
open import Function public | |
using (id ; flip) | |
renaming (_∘′_ to _∘_) |
module EncodeDecode where | |
open import Agda.Builtin.Char | |
using (Char) | |
renaming ( primCharToNat to ord | |
; primNatToChar to chr | |
) | |
open import Agda.Builtin.Equality | |
using (_≡_ ; refl) |
module STLCSemantics where | |
-------------------------------------------------------------------------------- | |
-- Types | |
infixr 7 _⇒_ | |
data Type : Set | |
where |