leanprover-community/NNG4

Rip out Proposition world

Closed this issue · 1 comments

The proposal is that we rip out function world, proposition world, and advanced proposition world, and then we have the problem that advanced addition world (and adv multiplication and inequality world) uses tactics which have not yet been taught, so they need to be taught within advanced addition world.

Let's focus on advanced addition world. What needs to be done here is that we need to see which tactics are being used in that world which were taught in the ripped-out worlds.

I take it you've done this now.