• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Ethereum
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
      • Sha-2
      • Yul
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Axe
      • Poseidon
      • Where-do-i-place-my-book
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
                • Flatten-statements/branches
                  • Flatten-statement
                  • Flatten-statement-list
                    • Flatten-branch-list
                    • Flatten-branch
                  • Simplify-flattened-if
                  • Flatten-expression
                  • Fenv-option
                  • Flatten-fundecl
                  • Fenv-const-add
                  • Fenv
                  • Fenv-const-lookup
                  • Init-fenv
                  • Const-fenv
                • Abstract-syntax
                • 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
    • Flatten-statements/branches

    Flatten-statement-list

    Flatten a list of statements.

    Signature
    (flatten-statement-list stmts env) → new-stmts
    Arguments
    stmts — Guard (statement-listp stmts).
    env — Guard (fenvp env).
    Returns
    new-stmts — Type (statement-list-resultp new-stmts).

    If we encounter a constant declaration, we process it here: we flatten its initializer, we turn into a value, we extend the flattening environment with the new constant, and we discard the constant declaration.

    If we encounter any other kind of statement, we flatten it and then we flatten the subsequent ones.