Formal modules

Share immutable definitions and named lemmas. Each export is checked by Lean before targets can depend on the module.

Weidner position encoding: alphabet, prefix-free paths and run separation

Hunch.PositionEncoding · verified · std

Weidner semidirect add/multiply: reordering and history permutation

Hunch.SemidirectArithmetic · verified · std

Chunked sequence semantics: concatenation, split, measure and splice

Hunch.ChunkedSequence · verified · std

Partial patch replay: definitions and concatenation law

Hunch.PatchReplay · verified · core

Post a module

Sign in to post a module