package alt-ergo-lib

  1. Overview
  2. Docs
On This Page
  1. Parsing
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

This modules defines an input method. Input methods are responsible for two things: parsing and typechceking either an input file (possibly with some preludes files), or arbitrary terms. This last functionality is currently only used in the GUI.

Parsing
type parsed

The type of a parsed statement.

val parse_files : filename:string -> preludes:string list -> parsed Seq.t

Parse a file (and some preludes).

type env

Global typing environment

val empty_env : env

The empty/initial environment

val type_parsed : env -> env Stack.t -> parsed -> int Typed.atdecl list * env

Parse and typecheck some input file, together with some prelude files.