tydeu Goto Github PK

checkdecls

Tiny Lean library to check existence of declarations

cmakejuce

CMake helper files for Juce projects

cve-search

cve-search - a tool to perform local searches for known vulnerabilities

doc-gen4

Document Generator for Lean 4

folktale

Knights and Knaves logic puzzles formalized in Lean 4.

ghc-proposals

Proposed compiler and language changes for GHC and GHC/Haskell

lake-cloud-test

A repository used to test Lake cloud builds.

lean-blake3

Lean4 bindings to the Blake3 (unfinished)

lean4

Lean 4 programming language and theorem prover

lean4-alloy

Write C shims from within Lean code.

lean4-betternumlits

A more flexible alternative macro expansion for Lean 4's numeric literals.

lean4-itertools

A Lean 4 library for iterators.

lean4-metaprogramming-book

lean4-papyrus

An LLVM interface for Lean 4. (WIP)

lean4-partax

Lean 4 library of tools for parsing and compiling syntax and parser definitions.

lean4-rffid

An example of using a Lean library with a Mathlib dependency in C.

lean4checker

Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.

leaninfer

Neural Network Inference in Lean 4

leanpy

Python in Lean 4

lyre

Lean IR as Lean syntax

mathport

Mathport is a tool for porting Lean3 projects to Lean4

msgpack

MessagePack is an extremely efficient object serialization library. It's like JSON, but very fast and small.

ntptutorial

Tutorial on neural theorem proving

pgpy

Pretty Good Privacy for Python

proofwidgets4

Helper toolkit for creating your own Lean 4 UserWidgets

socket.lean

sockets for Lean 4

std4

Standard Library for Lean 4

vscode-lean4