the blueprint show 'compile' not from the repo environment but a combination of mathlib and the repo env - its unclear how to connect code with blueprint
honestly - from en engineering persctive the minimal compile might not be a bad idea, but the link should return where the code is written
the blueprint show 'compile' not from the repo environment but a combination of mathlib and the repo env - its unclear how to connect code with blueprint
honestly - from en engineering persctive the minimal compile might not be a bad idea, but the link should return where the code is written