Lapinot Lapin0t

Lapin0t / test.agda

Last active December 16, 2021 23:14

dissection

	module test where

	data ty : Set where
	unit : ty
	_⇒_ : ty → ty → ty

	data env : Set where
	∅ : env
	_▸_ : env → ty → env

2 files
0 forks
0 comments
1 star

Lapin0t / Jigger.agda

Created January 10, 2024 17:55

A very cute demo of smart constructors for pure λ-calculus (some sort of HOAS to intrinsically scoped De-Bruijn transform) by Conor McBride which i ported to Coq.

	-- Source: Conor McBride
	-- https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
	module Jigger where

	data Nat : Set where
	zero : Nat
	suc : Nat -> Nat

	_+_ : Nat -> Nat -> Nat
	zero + n = n

OlderNewer