Skip to main content

parse_import_decl

Function parse_import_decl 

Source
pub fn parse_import_decl(input: &str) -> Option<ImportDecl>
Expand description

Parse a single import line.

Supported syntaxes:

  • import Mathlib.Algebra.Ring
  • import Mathlib.Algebra.Ring as MAR
  • import Mathlib.Algebra.Ring (add, mul)

Returns None if the line does not start with import or the module path is malformed.