Skip to content

Instantly share code, notes, and snippets.

View JacquesCarette's full-sized avatar

Jacques Carette JacquesCarette

View GitHub Profile
@AndrasKovacs
AndrasKovacs / ImpredTmAlg.agda
Last active June 29, 2022 14:23
Impredicative encodings as term algebra constructions
{-# OPTIONS --type-in-type #-}
open import Relation.Binary.PropositionalEquality
renaming (cong to ap; sym to infixl 6 _⁻¹; subst to tr; trans to infixr 4 _◾_)
open import Data.Product
renaming (proj₁ to ₁; proj₂ to ₂)
--------------------------------------------------------------------------------
NatAlg : Set
@neel-krishnaswami
neel-krishnaswami / abt
Last active June 15, 2021 21:17
Abstract binding trees implementation
(* -*- mode: ocaml; -*- *)
module type FUNCTOR = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}
type var = string