		Search-engine friendly clone of the ACL2 documentation.

Pfcs

Parser-interface

API functions for parsing PFCS specifications.

This section defines API functions for parsing PFCS specifications from :

an ACL2 string (in UTF-8)

By "parsing", we mean lexing, tokenization, and parsing. We define functions that output CSTs and ASTs, so we honorarily include syntax abstraction as part of the parsing interface.

Subtopics

Parse-from-string-to-cst: Parse UTF-8 ACL2 string into a PFCS system in CST form.
Parse: Parse UTF-8 ACL2 string into a PFCS system in AST form.