Skip to main content

parse_file

Function parse_file 

Source
pub fn parse_file(source: &str) -> ParseResult<Vec<Located<Decl>>>
Expand description

Parse all top-level declarations from an OxiLean source string.

This is the top-level wrapper for parsing a complete source file. It lexes the source, then calls parse_decl in a loop until EOF, collecting all successfully parsed declarations.

§Errors

Returns Err with a description string on the first parse error. Unlike parse_source_file, this function stops at the first error rather than attempting to recover.

§Example

use oxilean_parse::parse_file;

let source = "def foo : Nat := 0";
let decls = parse_file(source)?;
assert_eq!(decls.len(), 1);