Almost empty top folders

Stream: general

[Yaël Dillies]

system and testing both have very little content (1 and 4 files respectively). Are people opposed to renaming system.random.basic to data.random and move everything intesting.slim_check. to tactic.slim_check.?

[Scott Morrison]

I would guess testing/slim_check is not under either src/tactic or test because @Simon Hudon arranged so that it was all non-meta code.

[Scott Morrison]

One thing to consider is what will happen to it during the port to Lean 4. If it is under src/tactic or test it won't be automatically translated. (We could still run mathport on it, but it won't be part of the automatic workflow.)

[Yaël Dillies]

I think either is low priority, so you tell me.