Pinned Loading

1. bloomberg/crane bloomberg/crane Public

   Extraction of Rocq code to valid, performant, and memory-safe, modern C++ code.

   OCaml 1

2. bloomberg/game-trees bloomberg/game-trees Public

   Functions and proofs about game trees in Rocq, implemented as rose trees.

   Rocq Prover 9

3. proof-tree-builder/proof-tree-builder.github.io proof-tree-builder/proof-tree-builder.github.io Public

   A web-based graphical proof assistant for LK and Hoare logic.

   JavaScript 37 3

4. hezarfen hezarfen Public archive

   a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

   Idris 121 3

5. latex-unicoder.vim latex-unicoder.vim Public

   A plugin to type Unicode chars in Vim, using their LaTeX names.

   Vim Script 90 14

6. dilim dilim Public

   A structure editor for a simple functional programming language, with Vim-like shortcuts and commands.

   Rust 16