{{ message }}

Instantly share code, notes, and snippets.

# Miëtek Bak‏ mietek

Last active Aug 15, 2020 — forked from davidad/0_0_1.v
There is exactly one way to choose 0 elements from the empty set.
View Choose.agda
 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)
Created Jun 17, 2020 — forked from bitmappergit/lisp15.lisp
View lisp15.lisp
 (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)
Last active Aug 13, 2019 — forked from EdNutting/Irrelevance-Issue.agda
View Irrelevance-Issue.agda
 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
Created Jul 16, 2019
Erlang is magic!
View magic.erl
 -module(magic). -export([loop/0, start/0]). loop() -> receive Fun -> Fun(), loop() end.
Created Jul 12, 2019
Keybase proof
View keybase.md

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

Last active Jun 30, 2019 — forked from AndrasKovacs/SystemF.agda
Embedding of predicative polymorphic System F in Agda.
View SystemF.agda
 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
Last active Feb 18, 2018
Preordered sets using squashed types or explicit uniqueness
View Proset.agda
 module Proset where open import Agda.Primitive public using (_⊔_) open import Agda.Builtin.Equality public using (_≡_ ; refl) --------------------------------------------------------------------------------
Last active Dec 4, 2017
First meaningful use of irrelevance
View Category.agda
 module Category where open import Agda.Primitive public using (Level ; _⊔_) renaming (lzero to ℓ₀) open import Function public using (id ; flip) renaming (_∘′_ to _∘_)
Created Nov 30, 2017
Converting between strings and natural numbers
View EncodeDecode.agda
 module EncodeDecode where open import Agda.Builtin.Char using (Char) renaming ( primCharToNat to ord ; primNatToChar to chr ) open import Agda.Builtin.Equality using (_≡_ ; refl)
Last active Nov 10, 2017
Materials for my Haskell.SG talk on 9 November 2017
View STLCSemantics.agda
 module STLCSemantics where -------------------------------------------------------------------------------- -- Types infixr 7 _⇒_ data Type : Set where