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

ast_export

AST export from Lean 4

bors-ng

👁 A merge bot for GitHub Pull Requests

cadical

CaDiCaL SAT Solver

cmark.lean

cookie-monster

Javascript Cookie Library

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

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

isabelle

Fork of https://isabelle-dev.sketis.net so I can use git

isabelle-rs

Parser for isabelle database files

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