Skip to content

Instantly share code, notes, and snippets.

mietek / Choose.agda
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)
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)
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
mietek / magic.erl
Created Jul 16, 2019
Erlang is magic!
View magic.erl
-export([loop/0, start/0]).
loop() ->
Fun ->
mietek /
Created Jul 12, 2019
Keybase proof

Keybase proof

I hereby claim:

  • I am mietek on github.
  • I am mietek ( on keybase.
  • I have a public key ASC7JOFEAXt8XpqQVAUKRgl6x8YnzqyEnigshYRK-_71XQo

To claim this, I am signing this object:

mietek / SystemF.agda
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
mietek / Proset.agda
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)
mietek / Category.agda
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 _∘_)
mietek / EncodeDecode.agda
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)
mietek / STLCSemantics.agda
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