Skip to content

Instantly share code, notes, and snippets.

View Lapin0t's full-sized avatar

Lapinot Lapin0t

47 followers · 26 following
View GitHub Profile
@Lapin0t
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
@Lapin0t
Lapin0t / maybe_iter.v
Created July 23, 2025 11:05
Unguarded iteration of a weak maybe monad
Set Primitive Projections.
From Equations Require Import Equations.
Set Equations Transparent.
Record maybe (X : Type) := {
dom : Prop ;
val : dom -> X ;
}.
Arguments dom {X}.
@Lapin0t
Lapin0t / vec_rev.v
Last active November 11, 2025 10:24
Vector reversal in a couple lines.
From Stdlib Require Import Vector.
Notation vec := Vector.t.
Arguments nil {A}.
Arguments cons {A} _ {n}.
(* For some reason cons has the length argument after the head argument, which
will be cumbersome here. *)
Definition cons' {A} n (x : A) (xs : vec A n) : vec A (S n) := cons x xs.
Arguments cons' {_} _ _ _ /.