Search-engine friendly clone of the
ACL2 documentation
.
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
Identifiers
Types
Struct-init
Branch
Statements
Asgop
Constdecl
Console
Vardecl
Vardecl-result
Statement-result
Statement-list-result
Constdecl-result
Console-result
Branch-result
Branch-list-result
Asgop-result
Asgop-to-binop
Statement-fixtypes
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
Statements
Leo statements.
Here we formalize an abstract syntactic representation of all the Leo statements.
Subtopics
Asgop
Fixtype of Leo assignment operators.
Constdecl
Fixtype of constant declarations.
Console
Fixtype of Leo console calls.
Vardecl
Fixtype of variable declarations.
Vardecl-result
Fixtype of errors and Leo variable declarations.
Statement-result
Fixtype of errors and Leo statement.
Statement-list-result
Fixtype of errors and lists of Leo statements.
Constdecl-result
Fixtype of errors and Leo constant declarations.
Console-result
Fixtype of errors and Leo console function calls.
Branch-result
Fixtype of errors and Leo branches.
Branch-list-result
Fixtype of errors and lists of Leo branches
Asgop-result
Fixtype of errors and Leo assignment operators.
Asgop-to-binop
Map each Leo compound assignment operator to the corresponding binary operator.
Statement-fixtypes
Mutually recursive fixtypes of Leo statements.