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

mietek

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

mietek

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