A WIP definitional (co)datatype package for Lean4
-
Updated
Oct 23, 2025 - Lean
A WIP definitional (co)datatype package for Lean4
Evaluation of typed terms in Agda using the Delay monad.
TSC: Recognize and measure triadic coherence (H/V/D) via S₃-invariant protocol, witnesses, and C_Σ scoring. Coherence → Philosophy → Math → Engineering.
a formalisation of the functional pearl "Enumerating the Rationals" by Gibbons, Lester and Bird in Coq
Code and slides for my talk presented at the seminar.
CoInduction Termination and Category Theory
A small trick to get something similar to nested induction/coinduction in Coq, by nesting "finite coinductive types".
deciding regex equivalence with automata theory
Add a description, image, and links to the coinduction topic page so that developers can more easily learn about it.
To associate your repository with the coinduction topic, visit your repo's landing page and select "manage topics."