Function document_path 

pub fn document_path(target_lean: &str) -> String

The document’s file name for a Lean target: its name with anything outside letters, digits, _, - and . written as _, then .lg.