文件列表:

.envrc (10, 2023-11-20)
FormalSystems.lean (277, 2023-11-20)
FormalSystems/ (0, 2023-11-20)
FormalSystems/Chomsky/ (0, 2023-11-20)
FormalSystems/Chomsky/ContextFree/ (0, 2023-11-20)
FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean (4495, 2023-11-20)
FormalSystems/Chomsky/Grammar.lean (8440, 2023-11-20)
FormalSystems/Chomsky/Regular/ (0, 2023-11-20)
FormalSystems/Chomsky/Regular/DFA.lean (7639, 2023-11-20)
FormalSystems/Chomsky/Regular/NFA.lean (6373, 2023-11-20)
FormalSystems/Chomsky/Regular/Nerode.lean (5587, 2023-11-20)
FormalSystems/Chomsky/Regular/PowersetConstruction.lean (4199, 2023-11-20)
FormalSystems/Chomsky/Regular/RegularGrammar.lean (8419, 2023-11-20)
FormalSystems/Chomsky/Regular/TotalDFA.lean (3928, 2023-11-20)
FormalSystems/Computability/ (0, 2023-11-20)
FormalSystems/Computability/Loop.lean (6630, 2023-11-20)
FormalSystems/Preliminaries/ (0, 2023-11-20)
FormalSystems/Preliminaries/Alphabet.lean (296, 2023-11-20)
FormalSystems/Preliminaries/FinDenumerable.lean (4074, 2023-11-20)
FormalSystems/Preliminaries/Fold.lean (1795, 2023-11-20)
FormalSystems/Preliminaries/Language.lean (6449, 2023-11-20)
FormalSystems/Preliminaries/Word.lean (3950, 2023-11-20)
LICENSE (11353, 2023-11-20)
flake.lock (4487, 2023-11-20)
flake.nix (2567, 2023-11-20)
lake-manifest.json (1497, 2023-11-20)
lakefile.lean (180, 2023-11-20)
lean-toolchain (24, 2023-11-20)

# Formale Systeme in LEAN This repo contains the approach of formalizing the undergraduate Lecture ["Formale Systeme"](https://github.com/knowsys/FormaleSysteme) using [LEAN4](https://github.com/leanprover/lean4). The project started and still emerges mostly through student projects. You are welcome to participate, just contact us! ## Notes on Setup: Using `elan` / `lake`: ``` lake build ``` This will download mathlib4 and build the project. Currently it might still break, because mathlib4 has no releases yet. (Todo: update this when mathlib4 has a release)

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：