digama0 Goto Github PK

a-mir-formality

a PLT redex model of MIR and its type system

advent-of-code

The Advent of Code programming puzzles in Lean

annotate-snippets-rs

Library for snippet annotations

asm_simulator

bors-ng

👁 A merge bot for GitHub Pull Requests

cadical

CaDiCaL SAT Solver

cmark.lean

cookie-monster

Javascript Cookie Library

coq-rs

A Coq .vo parser in Rust

dae-parser

Rust crate for parsing Collada DAE files

digama0.github.io

My personal website

doc-gen4

Document Generator for Lean 4

drat-trim

The DRAT-trim proof checker

dtt.mm

Metamath database for dependent type theory

flt

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

flypitch

formalabstracts

frat

DRAT proof processor

glium

Safe OpenGL wrapper for the Rust language.

gltf-rs

A crate for loading glTF 2.0

hz-to-mm0

HOL Zero to Metamath Zero translator

if_chain

Macro for writing nested `if let` expressions

itertools

Extra iterator adaptors, iterator methods, free functions, and macros.

json-java

A reference implementation of a JSON package in Java.

kremlin

Lean port of the CompCert project in Coq, for the KreMLin compiler

lafny

Some experiments in Dafny-like syntax in Lean 4

lake

Lean 4 build system and package manager with configuration files written in Lean.

lean

Lean Theorem Prover

lean-1

Lean Theorem Prover

lean-cache

Lean 4 build cache management tool