Repository navigation

Experiments about extracting random variables - #4

Draft

RemyDegenne wants to merge 14 commits into

mainfrom

Commits on Aug 31, 2026

extract random variables
RemyDegenne
committed
da7bf52
Update RandomDo.lean
gaetanserre
committed
719d74f
Merge branch 'main' into extractVars
gaetanserre
committed
7b530f4
Update RandomDo.lean
gaetanserre
committed
c876e38
Fix `Thompson.lean`
gaetanserre
committed
b06c1ed

Commits on Sep 4, 2026

add extend_space tactic
RemyDegenne
committed
11eaad3
mk_all
RemyDegenne
committed
db6a226
better extend_space: remove the old space
RemyDegenne
committed
feff0e0
use transfer tactic in alg_env_trace
RemyDegenne
committed
969f657
move tests to Test
RemyDegenne
committed
ab21c23
minor
RemyDegenne
committed
950a0ce
fix lint
RemyDegenne
committed
ae5f52f

Commits on Sep 16, 2026

improve transfer and extend_space tactics
RemyDegenne
committed
dd3e68f
improve algtrace
RemyDegenne
committed
d983f5d