baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-15 17:55:37 +01:00
parent 688a9b1892
commit 08b3a5dfbc
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/thue_morse2.v
View File

@ -12,6 +12,8 @@
- tm_step_cubefree (there is no cube in the sequence) - tm_step_cubefree (there is no cube in the sequence)
- tm_step_square_size (all squared factors of odd - tm_step_square_size (all squared factors of odd
length have length 1 or 3). length have length 1 or 3).
- tm_step_square_pos (length of the prefix has the same
parity than the length of the factor being squared)
*) *)
Require Import thue_morse. Require Import thue_morse.