pub fn prove_library(theorems: &[LibraryTheorem]) -> Vec<LibraryResult>Expand description
Discharge a library of theorems in citation order. Each theorem is proved from its own premises plus the conclusions of the (already-proved) theorems it cites, so a citation graph is walked exactly like the scraped Euclid dependency graph. Results are returned in the INPUT order. A citation of an unproved/failed theorem simply isn’t available as a premise (so the dependent proof fails too).