Olivier Binda

mm0-ification of set.mm

1

If I understand set.mm0 correctly, you suggest to remove ' axiom df_tru {x2: setvar}: $ wb wtru (wi (wal x2 (wceq (cv x2) (cv x2))) (wal x2 (wceq (cv x2)...

Scope name collisions will create weird bevavior/issues, hard to debug

1

The way used to name scopes will create awfull issues (hard to understand/debug) : You shouldn't use the class name for scopes like this : @Override public Context setUpContext(Path path,...