Pinned Repositories
aesop
White-box automation for Lean 4
ascent
logic programming in Rust
k_framework_tutorial_jp
k-framework日本語 (公式チュートリアルの非公式翻訳)
mathlib4-docs-ja
Mathlib4 docs の和訳リポジトリ
nanoda
A type checker for the Lean theorem prover
nanoda_lib
Library implementing type inference/checking functionality based on the Lean theorem prover
printiest
A pretty printer for Lean 4
second_opinion
timelib
A date and time library for Lean 4
type_checking_in_lean4
Type Checking in Lean 4
ammkrn's Repositories
ammkrn/nanoda_lib
Library implementing type inference/checking functionality based on the Lean theorem prover
ammkrn/type_checking_in_lean4
Type Checking in Lean 4
ammkrn/timelib
A date and time library for Lean 4
ammkrn/printiest
A pretty printer for Lean 4
ammkrn/second_opinion
ammkrn/mathlib4-docs-ja
Mathlib4 docs の和訳リポジトリ
ammkrn/aesop
White-box automation for Lean 4
ammkrn/ascent
logic programming in Rust
ammkrn/catala
Programming language for literate programming law specification
ammkrn/dada
I speak only of myself since I do not wish to convince, I have no right to drag others into my river, I oblige no one to follow me and everybody practices his art in his own way.
ammkrn/edit
ammkrn/helix
A post-modern modal text editor.
ammkrn/lake
Lean 4 build system and package manager with configuration files written in Lean.
ammkrn/lean4
Lean 4 programming language and theorem prover
ammkrn/lean4export
Plain-text declaration export for Lean 4
ammkrn/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
ammkrn/mathlib4
Work in progress mathlib port for lean 4
ammkrn/mm0
Metamath Zero specification language
ammkrn/nushell
A new type of shell
ammkrn/nushell.github.io
Nushell's main website, blog, book, and more
ammkrn/polars-book
Book documentation of the Polars DataFrame library
ammkrn/ropey
A utf8 text rope for manipulating and editing large texts.
ammkrn/rust-analyzer
A Rust compiler front-end for IDEs
ammkrn/souffle
Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
ammkrn/std4
Standard Library for Lean 4
ammkrn/taxing_digital_losses
Repository for the paper "Taxing Digital Asset Losses"
ammkrn/theorem_proving_in_lean4
Theorem Proving in Lean 4
ammkrn/ungrammar
ammkrn/webview_bug_demo
for vscode issue #130752
ammkrn/zero-to-nix
Zero to Nix is your guide to learning Nix and flakes. Created by Determinate Systems.