		Search-engine friendly clone of the ACL2 documentation.

Language

Abstract-syntax

Abstract syntax of Syntheto.

We formalize the abstract syntax of the language via recursive fixtypes, as commonly done.

This is just for an initial version of the language, which is expected to be extended and improved over time.

Subtopics

Expression: Fixtype of Syntheto expressions.
Expression-sum-field-list: Lift expression-sum-field to lists of field names.
Type: Fixtype of Syntheto types.
Binary-op: Fixtype of Syntheto binary operators.
Expression-product-field-list: Lift expression-product-field to lists of field names.
Abstract-syntax-operations: Operations on the Syntheto abstract syntax.
Function-definition-list->header-list: Lift function-definition->header to lists.
Type-definition-list->name-list: Lift type-definition->name to lists.
Initializer-list->value-list: Lift initializer->value to lists.
Function-header-list->name-list: Lift function-header->name to lists.
Typed-variable-list->type-list: Lift typed-variable->type to lists.
Typed-variable-list->name-list: Lift typed-variable->name to lists.
Branch-list->condition-list: Lift branch->condition to lists.
Alternative-list->name-list: Lift alternative->name to lists.
Function-specifier: Fixtype of Syntheto function specifiers.
Expression-variable-list: Lift expression-variable to lists.
Type-subset: Fixtype of Syntheto type subsets.
Field-list->type-list: Lift field->type to lists.
Field-list->name-list: Lift field->name to lists.
Function-specification: Fixtype of Syntheto function specifications.
Identifier: Fixtype of Syntheto identifiers.
Toplevel: Fixtype of Syntheto top-level constructs.
Function-definer: Fixtype of Syntheto function definers.
Function-header: Fixtype of Syntheto function headers.
Type-definer: Fixtype of Syntheto type definers.
Literal: Fixtype of Syntheto literals.
Type-product: Fixtype of Syntheto type products.
Function-definition: Fixtype of Syntheto function definitions.
Type-sum: Fixtype of Syntheto type sums.
Maybe-expression: Fixtype of optional Syntheto expressions.
Transform-argument-value: Fixtype of tagged transform argument value.
Transform: Fixtype of Syntheto transforms.
Theorem: Fixtype of Syntheto theorems.
Quantifier: Fixtype of Syntheto quantifiers.
Maybe-function-specification: Fixtype of optional function specifications.
Maybe-typed-variable: Fixtype of optional Syntheto typed-variables.
Maybe-type-definition: Fixtype of optional type definitions.
Maybe-function-header: Fixtype of optional function headers.
Maybe-function-definition: Fixtype of optional function definitions.
Maybe-type-sum: Fixtype of optional Syntheto type sums.
Maybe-type-subset: Fixtype of optional Syntheto type subsets.
Maybe-type-product: Fixtype of optional Syntheto type products.
Maybe-type-definer: Fixtype of optional type definers.
Maybe-theorem: Fixtype of optional theorems.
Maybe-type: Fixtype of optional Syntheto types.
Initializer: Fixtype of Syntheto field initializers.
Type-definition: Fixtype of Syntheto type definitions.
Alternative: Fixtype of Syntheto alternatives.
Unary-op: Fixtype of Syntheto unary operators.
Typed-variable: Fixtype of Syntheto typed variables.
Branch: Fixtype of Syntheto branches.
Field: Fixtype of Syntheto fields.
Transform-argument: Fixtype of Syntheto transform arguments.
Type-recursion: Fixtype of Syntheto type recursions.
Program: Fixtype of Syntheto programs.
Function-recursion: Fixtype of Syntheto function recursions.
Typed-variable-list: Fixtype of lists of Syntheto typed variables.
Toplevel-name
Toplevel-list: Fixtype of lists of Syntheto top-level constructs.
Initializer-list: Fixtype of lists of Syntheto field initializers.
Expression-fixtypes: Mutually recursive fixtypes for Syntheto expressions.
Toplevel-fn-names
Lookup-transform-argument
Function-definition-names
Type-definition-list: Fixtype of lists of Syntheto type definitions.
Transform-argument-list: Fixtype of lists of Syntheto transform arguments.
Function-header-list: Fixtype of lists of Syntheto function headers.
Function-definition-list: Fixtype of lists of Syntheto function definitions.
Alternative-list: Fixtype of lists of Syntheto type alternatives.
Type-list: Fixtype of lists of Syntheto types.
Identifier-set: Fixtype of osets of identifiers.
Identifier-list: Fixtype of lists of Syntheto identifiers.
Field-list: Fixtype of lists of Syntheto type fields.
Expression-list: Fixtype of lists of Syntheto expressions.
Branch-list: Fixtype of lists of Syntheto branches.
Extract-default-param-alist
Create-arg-defaults-table