• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
                • Expression
                • Syntax-abstraction
                • Statement
                • Files
                • Input-files
                  • Input-section-list->title-list
                  • Input-title-option
                  • Input-section-option
                  • Input-item
                  • Input-type
                  • Input-section
                  • Input-expression
                  • Input-title
                  • Input-file
                  • Input-section-option-result
                  • Input-section-list-result
                  • Input-type-result
                  • Input-title-result
                  • Input-title-option-result
                  • Input-section-result
                  • Input-item-result
                  • Input-item-list-result
                  • Input-file-result
                  • Input-expression-result
                  • Input-section-list
                  • Input-item-list
                  • Input-title-list
                • Identifiers
                • Types
                • Struct-init
                • Branch
                • Statements
                • Format-strings
                • Input-syntax-abstraction
                • Expressions
                • Output-files
                • Addresses
                • Literals
                • Characters
                • Expression-list
                • Statement-list
                • Output-syntax-abstraction
                • Struct-init-list
                • Branch-list
                • Annotations
                • Abstract-syntax-trees
                • Symbols
                • Keywords
                • Programs
                • Packages
                • Bit-sizes
              • Dynamic-semantics
              • Compilation
              • Static-semantics
              • Concrete-syntax
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-syntax

Input-files

Leo input files.

Besides files with code, formalized by file, Leo includes files with inputs. These are formalized here, in abstract syntax form, based on the ABNF input grammar.

Subtopics

Input-section-list->title-list
Lift input-section->title to lists.
Input-title-option
Fixtype of optional input titles.
Input-section-option
Fixtype of optional input sections.
Input-item
Fixtype of input items.
Input-type
Fixtype of input types.
Input-section
Fixtype of input sections.
Input-expression
Fixtype of input expressions.
Input-title
Fixtype of input titles.
Input-file
Fixtype of input files.
Input-section-option-result
Fixtype of errors and optional input sections.
Input-section-list-result
Fixtype of errors and lists of Leo input sections.
Input-type-result
Fixtype of errors and Leo input files.
Input-title-result
Fixtype of errors and Leo input titles.
Input-title-option-result
Fixtype of errors and optional input titles.
Input-section-result
Fixtype of errors and Leo input sections.
Input-item-result
Fixtype of errors and Leo input items.
Input-item-list-result
Fixtype of errors and lists of Leo input items.
Input-file-result
Fixtype of errors and Leo input files.
Input-expression-result
Fixtype of errors and Leo input expressions.
Input-section-list
Fixtype of input sections.
Input-item-list
Fixtype of input items.
Input-title-list
Fixtype of lists of input titles.