Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
78 commits
Select commit Hold shift + click to select a range
e8c772b
add files
BoltonBailey Jan 14, 2026
efa6880
refactor
BoltonBailey Jan 14, 2026
946f4a3
remove listblank content
BoltonBailey Jan 14, 2026
0c3b432
clean up
BoltonBailey Jan 17, 2026
630ce61
claude build/switch to reduces API
BoltonBailey Jan 17, 2026
4587a74
claude: remove sorries
BoltonBailey Jan 17, 2026
35558b8
delete evals junk
BoltonBailey Jan 17, 2026
1ef6182
clean whitespace
BoltonBailey Jan 17, 2026
6a2d234
TM0 -> SingleTapeTM
BoltonBailey Jan 17, 2026
68c6ae4
generalize alphabet
BoltonBailey Jan 17, 2026
6cb8c86
move blowuplemma earlier
BoltonBailey Jan 17, 2026
33d74e8
Stmt API
BoltonBailey Jan 17, 2026
24bd6de
clean up reduction
BoltonBailey Jan 17, 2026
21fe238
More comments
BoltonBailey Jan 22, 2026
9b61c24
Merge branch 'main' of github.com:leanprover/cslib into single-tape-t…
BoltonBailey Jan 23, 2026
ed9474b
rename to `BiTape` and `StackTape`
BoltonBailey Jan 23, 2026
99d9df6
clean up docs
BoltonBailey Jan 23, 2026
e69b48e
Merge branch 'main' of github.com:leanprover/cslib into single-tape-t…
BoltonBailey Jan 23, 2026
6aee1d9
lake exe mk_all --module
BoltonBailey Jan 23, 2026
4b0e241
update StackTape description
BoltonBailey Jan 23, 2026
7092768
clean up bitape file
BoltonBailey Jan 23, 2026
0711013
use relatesInSteps API
BoltonBailey Jan 23, 2026
a6a1c23
revert ReductionSystem/Basic
BoltonBailey Jan 23, 2026
7d8557b
refactor computer
BoltonBailey Jan 23, 2026
b1384f7
improve variable names
BoltonBailey Jan 23, 2026
faca3ff
claude refactor out time from composition functionality
BoltonBailey Jan 23, 2026
435971c
add private to lemmas
BoltonBailey Jan 23, 2026
6426bc5
rename helper lemmas
BoltonBailey Jan 23, 2026
50b6131
Merge branch 'main' into single-tape-turing-machines
BoltonBailey Jan 23, 2026
bacefc5
claude: uniformize the helper lemmas
BoltonBailey Jan 23, 2026
664f62c
Merge branch 'single-tape-turing-machines' of github.com:BoltonBailey…
BoltonBailey Jan 23, 2026
1576498
clean up helpers
BoltonBailey Jan 23, 2026
e348d76
further trim helpers
BoltonBailey Jan 23, 2026
c5231d9
remove vanilla computable
BoltonBailey Jan 23, 2026
b191ee9
rename fields
BoltonBailey Jan 23, 2026
c9ac367
public import Cslib.Init
BoltonBailey Jan 23, 2026
9286128
add note
BoltonBailey Jan 23, 2026
2ab4751
correct cons and provide API
BoltonBailey Jan 25, 2026
ccd4034
clean up tape apis
BoltonBailey Jan 25, 2026
ba47f4f
add docstrings
BoltonBailey Jan 25, 2026
a387696
more doc linter
BoltonBailey Jan 25, 2026
1a77e7c
imrove docs
BoltonBailey Jan 25, 2026
3d639c2
revert whitespace
BoltonBailey Jan 25, 2026
d14d5ee
clean up lines
BoltonBailey Jan 25, 2026
8b06d4a
use variables
BoltonBailey Jan 25, 2026
f7b6bbb
golfs
BoltonBailey Jan 25, 2026
19ebc8c
more golfs
BoltonBailey Jan 26, 2026
1361553
add movement lemmas
BoltonBailey Jan 26, 2026
4335852
golf
BoltonBailey Jan 26, 2026
4da0154
more line golfing
BoltonBailey Jan 26, 2026
f220ae0
clean up docstring
BoltonBailey Jan 26, 2026
aad3692
namespaces
BoltonBailey Jan 26, 2026
36615f3
Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
BoltonBailey Jan 30, 2026
90e6ac4
fix typeclass arg names
BoltonBailey Jan 30, 2026
f5b92e7
remove unneeded parens
BoltonBailey Jan 30, 2026
78733a8
use notation
BoltonBailey Jan 30, 2026
d7f384c
more bundled instances
BoltonBailey Jan 30, 2026
f5d0cfe
Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
BoltonBailey Jan 30, 2026
b5e035f
golf
BoltonBailey Jan 30, 2026
c3858fe
reorder args
BoltonBailey Jan 30, 2026
e6a2746
move args before :=
BoltonBailey Jan 30, 2026
0746a77
Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
BoltonBailey Jan 30, 2026
e356245
reorder proof
BoltonBailey Jan 30, 2026
9a08b4e
Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
BoltonBailey Jan 30, 2026
9a2190e
Merge branch 'single-tape-turing-machines' of github.com:BoltonBailey…
BoltonBailey Jan 30, 2026
3329685
Stmt becomes structure
BoltonBailey Jan 30, 2026
76e7c6e
clean up docs
BoltonBailey Jan 30, 2026
f45d40e
add doc
BoltonBailey Jan 30, 2026
1c251fb
add comment
BoltonBailey Jan 30, 2026
82ed427
add documentation on design
BoltonBailey Jan 30, 2026
a03c551
Merge branch 'main' of github.com:leanprover/cslib into single-tape-t…
BoltonBailey Jan 30, 2026
5516a25
ipossilbe instances removed
BoltonBailey Jan 30, 2026
4944e7a
lake exe mk_all
BoltonBailey Jan 30, 2026
97308fa
lake exe mk_all --module
BoltonBailey Jan 30, 2026
7c097a6
grind annotations
BoltonBailey Jan 30, 2026
600e016
some more grind lemmas
BoltonBailey Jan 30, 2026
b4704d1
more grind annotations
BoltonBailey Jan 31, 2026
ee79f80
scoped grind
BoltonBailey Jan 31, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Cslib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,11 @@ public import Cslib.Computability.Languages.Language
public import Cslib.Computability.Languages.OmegaLanguage
public import Cslib.Computability.Languages.OmegaRegularLanguage
public import Cslib.Computability.Languages.RegularLanguage
public import Cslib.Computability.Machines.SingleTapeTuring.Basic
public import Cslib.Foundations.Control.Monad.Free
public import Cslib.Foundations.Control.Monad.Free.Effects
public import Cslib.Foundations.Control.Monad.Free.Fold
public import Cslib.Foundations.Data.BiTape
public import Cslib.Foundations.Data.FinFun
public import Cslib.Foundations.Data.HasFresh
public import Cslib.Foundations.Data.Nat.Segment
Expand All @@ -40,6 +42,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal
public import Cslib.Foundations.Data.RelatesInSteps
public import Cslib.Foundations.Data.Relation
public import Cslib.Foundations.Data.Set.Saturation
public import Cslib.Foundations.Data.StackTape
public import Cslib.Foundations.Lint.Basic
public import Cslib.Foundations.Semantics.FLTS.Basic
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
Expand Down
Loading