Function check_metatheorems 

pub fn check_metatheorems(text: &str, file: Option<&str>) -> MetatheoremReport

Public API: evaluate text, then enumerate every relation that has a (mode ...) declaration plus matching (relation ...) clauses, and every definition that has a (define ...) declaration. Each candidate becomes a metatheorem result.

file is the source path used in evaluation diagnostics; it is optional and only affects the rendered span.