Skip to main content

parse_lean_name

logicaffeine_cli::interface::lean::intake

Function parse_lean_name 

Source 
pub fn parse_lean_name(text: &str) -> Result<Vec<Component>, Verdict>
Expand description

Parse a dotted Lean name as Lean prints it: components separated by ., a component that is not an identifier written «…», a component of digits numeric.