Input-execution
Execution of input files.
Executing an input file amounts to
evaluating its items to obtain inputs for the main function.
We formalize this defensively,
as for other aspects of the Leo dynamic semantics,
i.e. we also check that the values and sorts match
the types and sorts of the main parameters.
Subtopics
- Eval-input-item-list
- Evaluate a list of input items.
- Eval-input-item
- Evaluate an input item.
- Funarg
- Fixtype of function arguments.
- Funarg-option
- Fixtype of optional function arguments.
- Eval-input-section-list
- Evaluate a list of input sections.
- Eval-input-section
- Evaluate an input section.
- Eval-input-file
- Evaluate an input file.
- Funarg-result
- Fixtype of errors and function arguments.
- Funarg-list-result
- Fixtype of errors and listf of function arguments.
- Funarg-list
- Fixtype of lists of function arguments.
