Skip to content

Instantly share code, notes, and snippets.

Miëtek Bak‏ mietek

Block or report user

Report or block mietek

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
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
mietek / magic.erl
Created Jul 16, 2019
Erlang is magic!
View magic.erl
-module(magic).
-export([loop/0, start/0]).
loop() ->
receive
Fun ->
Fun(),
loop()
end.
@mietek
mietek / keybase.md
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:

@mietek
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
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
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
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
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
where
View RenSubFirstDraft.agda
-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand
{-# OPTIONS --no-positivity-check #-}
module RenSubFirstDraft where
View RenSub.agda
-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand
{-# OPTIONS --no-positivity-check #-}
module RenSub where
open import Function public
You can’t perform that action at this time.