Skip to content

Instantly share code, notes, and snippets.

View jiribenes's full-sized avatar

Jiří Beneš jiribenes

View GitHub Profile
@jiribenes
jiribenes / Compiler.agda
Last active January 6, 2022 11:01
simple stack compiler&decompiler :)
{-# OPTIONS --without-K --safe #-}
module Compiler where
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
infixr 5 _∷_
{-# BUILTIN LIST List #-}

Keybase proof

I hereby claim:

  • I am jiribenes on github.
  • I am jiribenes (https://keybase.io/jiribenes) on keybase.
  • I have a public key whose fingerprint is 5E34 7775 E880 5402 3872 62BD D5F9 58FA CE02 3AF5

To claim this, I am signing this object: