issues
search
knowsys
/
Formale-Systeme-in-LEAN
LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP)
Apache License 2.0
8
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Upgrade to Lean 4.11.0
#30
monsterkrampe
closed
1 month ago
0
Improve "inner" constructor for DerivationTree
#29
monsterkrampe
opened
1 month ago
0
Avoid tactic based definitions
#28
monsterkrampe
closed
1 month ago
0
Avoid Construction of Non-Prop Types through Tactics
#27
monsterkrampe
closed
1 month ago
1
Upgrade to Lean 4.11.0
#26
monsterkrampe
closed
1 month ago
0
Leos work on context free grammars
#25
monsterkrampe
closed
1 month ago
0
Upgrade to Lean (and mathlib) 4.7.0
#24
monsterkrampe
closed
6 months ago
0
Upgrade to Lean 4.6.1
#23
monsterkrampe
closed
7 months ago
0
Rename N/DFA GeneratedLanguage to AcceptedLanguage
#22
monsterkrampe
closed
7 months ago
0
Update Mathlib Note in README.md
#21
monsterkrampe
closed
8 months ago
0
Upgrade Lean to v4.5.0
#20
monsterkrampe
closed
9 months ago
0
Use elan for CI without nix
#19
monsterkrampe
closed
9 months ago
0
Fix Nix Build
#18
monsterkrampe
closed
1 month ago
1
Upgrade to Lean v4.4.0
#17
monsterkrampe
closed
9 months ago
6
update lean to 4.2.0 / stable
#16
matzemathics
closed
11 months ago
0
define DFA.toTotalDFA, and prove it accepts the same language
#15
matzemathics
closed
11 months ago
0
setup ci
#14
matzemathics
closed
11 months ago
7
prove, that the canonical automaton accepts the right language
#13
matzemathics
closed
11 months ago
0
Theorems for total DFAs and transitively closed transition functions
#12
matzemathics
closed
11 months ago
1
normalize grammar.lean file
#11
matzemathics
closed
11 months ago
0
define canonical automata, based on myhill-nerode congruence
#10
matzemathics
closed
11 months ago
0
simplify the definition of ContextFreedom
#9
matzemathics
closed
1 year ago
0
Implement evaluation of loop programs
#8
monsterkrampe
closed
1 year ago
0
update lean and mathlib to current versions
#7
matzemathics
closed
1 year ago
0
Loop
#6
matzemathics
closed
1 year ago
0
Powerset construction: From NFA to DFA
#5
matzemathics
closed
1 year ago
0
Grammar to NFA
#4
matzemathics
closed
1 year ago
0
Structural rewrite, using mathlib4
#3
matzemathics
closed
1 year ago
1
Weird type coercion of Inductive types
#2
matzemathics
closed
1 year ago
2
Show that FinDenumerable is equiv to Fin
#1
monsterkrampe
closed
1 year ago
1