Mulit tape sim - #174

Draft

crei wants to merge 59 commits into

mainfrom

Commits on Mar 10, 2026

Update Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

crei
and
chenson2018
authored
cb9e7a3
Extract common parts.
crei
committed
cc78278
Simplify definitions and proofs.
crei
committed
07d7bcd
Use "@[expose] public section"
crei
committed
841be7f
Update Cslib.lean
crei
committed
abac0f1
Add missed file.
crei
committed
ae6c498

Commits on Mar 19, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
b38b929
fix import.
crei
committed
7401a21

Commits on Apr 18, 2026

Function view for tapes.
crei
committed
f57bb82

Commits on Apr 20, 2026

Apply suggestions from code review

crei
and
chenson2018
authored
642162c
Simplify some proofs and add annotations.
crei
committed
be6855a

Commits on Apr 30, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
93b6704
Move "expose" command below module-level documentation.
crei
committed
3110f77

Commits on May 5, 2026

Commits on May 6, 2026

feat(Foundations/Data/Relation): strongly normalising elements of a type equipped with a relation (#549)

authored
cdfe655

Commits on May 7, 2026

feat: Modal Logic (#528)

fmontesi
and
chenson2018
authored
ab16df6

Commits on May 11, 2026

feat: some lemmas about Euclidean relations (#557)
chenson2018
authored
b37c36e
feat(MachineLearning/PACLearning): definitions (#492)

SamuelSchlesinger
and
fmontesi
authored
ca0e27c
feat(Cryptography/SecretSharing): Shamir's secret sharing (#495)

SamuelSchlesinger
and
fmontesi
authored
57e5054
ci: use `INFO=true` for weekly linting (#526)
chenson2018
authored
2e5e64d
Apply suggestions from code review

crei
and
chenson2018
authored
283bc0b

Commits on May 12, 2026

chore(ci): pin lint-style-action to a SHA instead of @main (#561)

kim-em
and
claude
authored
28a8f5e
chore(ci): bump lint-style-action pin off reverted commit (#562)

kim-em
and
claude
authored
b3c5575
doc: fix missing '$' (#564)
lengyijun
authored
608cbe1

Commits on May 20, 2026

Commits on May 21, 2026

refactor: use `Option State` rather than `Sum State Unit` in `LTS.totalize` construction (#584)
ctchou
authored
f3c2894

Commits on May 23, 2026

feat: FullEta.step_lc_l (#589)

lengyijun
and
chenson2018
authored
6cc5327
doc: link to Mathlib AI policy in CONTRIBUTING.md (#593)

chenson2018
and
fmontesi
authored
85518e6

Commits on May 24, 2026

chore: Bump `mathlib` dependency to d8de6b6 (#552)

mathlib-nightly-testing[bot]
and
chenson2018
authored
107a51d

Commits on May 26, 2026

feat(locallynameless): signature of fv theorems (#588)

lengyijun
and
chenson2018
authored
c6bb800
feat: subst_refl (#599)
lengyijun
authored
28e0b17
chore: bump toolchain to v4.30.0 (#601)
Garmelon
authored
c7944a9

Commits on May 27, 2026

refactor: change the simpNF for FreeM (#417)
eric-wieser
authored
d780a2a

Commits on May 28, 2026

Commits on May 29, 2026

Commits on Jun 1, 2026

feat(FLP): distributed algorithms for solving the consensus problem (#556)
ctchou
authored
43f68e9

Commits on Jun 2, 2026

Commits on Jun 3, 2026

Merge branch 'tapes_as_functions' into mulit-tape-sim
crei
committed
098627f

Commits on Jun 4, 2026

copy semantics.
crei
committed
c684b79
more sim
crei
committed
ea15156
Do not use BiTape for input.
crei
committed
3d406b7
simulation
crei
committed
d8fef55

Commits on Jun 5, 2026

more sim
crei
committed
d07c117
Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
398ad91
Make move optional.
crei
committed
6847a62
Merge branch 'multi-tape-tm' into mulit-tape-sim
crei
committed
fd6573c

Commits on Jun 7, 2026

sim
crei
committed
2681d91