Automatically Generate EQ Taclets - #3949

Merged

Drodt merged 17 commits into

mainfrom

Aug 9, 2026

Commits on Jul 30, 2026

Commits on Jul 31, 2026

Generate missing rule
Drodt
committed
b91b3fc
Fix one EQ taclet
Drodt
committed
234dd8d
Generate missing rules
Drodt
committed
795de27
Document
Drodt
committed
41507bc
Fix copy method
Drodt
committed
fce1b92
Check that EQ term is actually in \find (and fix rules)
Drodt
committed
42f2bcb
Add simplify rule set to lenOfSeqSub
Drodt
committed
349497e
Update taclet names in strings and SMT settings
Drodt
committed
306168b

Commits on Aug 7, 2026

Generalize generator concept
Drodt
committed
eba2986
Fix \EQ generator
Drodt
committed
1f075db
Regenerate oracle for taclet equality
Drodt
committed
a02a6ce