rzrn — Vaya

ground_zero. Ground Zero: Lean 4 HoTT Library

84

anders. Anders: Cubical Type Checker

23

loria. Minetest subgame

21

lean4-categories. Category Theory & Cobordism Categories in Lean 4

16

leanbot. IRC-bot written in Lean (https://leanprover.github.io/)

10

tigerspades. BetterSpades for PowerPC Mac OS X

10

aos-milsim. Kind of Military Simulator Game built upon https://github.com/rzrn/piqueserver2

10

bravo. Castle Bravo: Experimental HoTT Implementation

9

9aout. Running native amd64 Plan 9 binaries through Syscall User Dispatch (Linux 5.11+)

9

solar. Very simple solar system simulator.

6

starfish_prime. Starfish Prime: Lisp Flavoured LCF

5

emacs-qsharp-mode. GNU/Emacs Q# mode

4

dtt-cpp-templates. Dependent Type Theory on C++ Templates

4

lean-vcpu. Lean

4

general-recursive-functions. Toy point free language implementing GRF

3

romeo. Castle Romeo: Experimental Theorem Prover for Category Theory

3

JackSharp. C# bindings for Jackd

3

hypertest. Hyperbolic Minetest-like game

3

hurricane. Hurricane: HoTT-I Type System

3

BetterSpades. C++

2

hask. Continuation of work on https://github.com/billpmurphy/hask, Haskell language features and standard libraries in pure Python.

2

acme. Acme Text Editor (detached from plan9port)

2

fennel-vscode.

2

principia. Principia: Metamath-like Logician Language

2

hrin. An attempt to reinvent the garbage collector

2

piqueserver2. https://github.com/piqueserver/piqueserver fork

1

lambda. Untyped lambda calculus implemented in Lean

1

halite2. C++

1

lambda-limbo. Implementation of λ calculus in Limbo

1

test.

1

gnustep-embed. Lightweight GNUstep/Cocoa wrapper for XTerm/Rxvt

1

SpiceJack. F#

1

sound-experiments. Sound experiments

1

fennel-types.

1

melting_point. Some mathematical stuff (in Lean)

1

coqbot. IRC‐Bot on Coq. Proof of concept.

1

cubicaltt-vscode.

1

bump. Lean 4 Package Manager

1