Currently, claim and define declarations can be interleaved in ways that would lead to circular definitions. I don't want to rely on loop detection to determine well-foundedness of definitions, because I think this might still allow things that aren't actually justified in the mathematics.
Instead, I think that a define declaration should be elaborated with only the scope visible prior to the corresponding claim.