		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Files

Leo files.

Here we formalize an abstract syntactic representation of Leo files, including the top-level declarations that form the files.

Subtopics

Funparam-list->name-list: Lift funparam->name to lists.
Fundecl: Fixtype of Leo function/transition declarations.
Var/const-sort: Fixtype of sorts of variables and constants.
Structdecl: Fixtype of struct and record declarations.
File: Fixtype of Leo files.
Finalizer-option: Fixtype of optional Leo finalizer blocks.
Topdecl: Fixtype of Leo declarations at the top level in a program.
Mappingdecl: Fixtype of mapping declarations.
Fundecl-option: Fixtype of optional Leo function declarations.
Finalizer: Fixtype of Leo finalizer blocks.
Funparam: Fixtype of Leo function parameters.
Fun-sort: Fixtype of sorts of Leo functions.
Programdecl: Fixtype of Leo program declarations.
Compdecl: Fixtype of struct component declarations.
Var/const-sort-result: Fixtype of errors and Leo variable or constant sorts.
Topdecl-list-result: Fixtype of errors and lists of Leo top-level declarations.
Programdecl-list-result: Fixtype of errors and lists of Leo program declarations.
Importdecl-list-result: Fixtype of errors and lists of Leo import declarations.
Funparam-list-result: Fixtype of errors and lists of Leo function parameters.
Finalizer-option-result: Fixtype of errors and optional Leo finalizer blocks.
Compdecl-list-result: Fixtype of errors and lists of Leo struct component declarations.
Topdecl-result: Fixtype of errors and Leo top-level declarations.
Structdecl-result: Fixtype of errors and Leo struct declarations.
Programdecl-result: Fixtype of errors and Leo program declarations.
Mappingdecl-result: Fixtype of errors and Leo mapping declarations.
Importdecl-result: Fixtype of errors and Leo import declarations.
Importdecl: Fixtype of Leo import declarations.
Funparam-result: Fixtype of errors and Leo function parameters.
Fundecl-result: Fixtype of errors and Leo function declarations.
Fun-sort-result: Fixtype of errors and Leo function sorts.
Finalizer-result: Fixtype of errors and Leo finalizer blocks.
Compdecl-result: Fixtype of errors and Leo struct component declarations.
File-result: Fixtype of errors and Leo files.
Funparam-list: Fixtype of lists of Leo function parameters.
Programdecl-list: Fixtype of lists of Leo program declarations.
Importdecl-list: Fixtype of lists of Leo import declarations.
Compdecl-list: Fixtype of lists of struct component declarations.
Var/const-sort-list: Fixtype of lists of variable and constant sorts.
Topdecl-list: Fixtype of Leo top-level declarations.
Fundecl-list: Fixtype of lists of Leo function declarations.