• 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
              • Dynamic-semantics
                • Execution
                  • Exec-expressions/statements
                  • Init-for-loop
                  • Exec-file-main
                  • Update-variable-value-in-scope-list
                  • Step-for-loop
                  • Update-variable-value-in-scope
                  • Expr-value-to-value
                  • Exec-binary
                  • Exec-expression
                  • Init-vcscope-dinfo-call
                  • Value?+denv
                  • Exec-statement
                  • End-of-for-loop-p
                  • Expr-value
                  • Evalue+denv
                    • Evalue+denv-fix
                    • Evalue+denv-equiv
                    • Make-evalue+denv
                    • Evalue+denv->evalue
                    • Evalue+denv->denv
                    • Change-evalue+denv
                    • Evalue+denv-p
                  • Write-location
                  • Read-location
                  • Exec-for-loop-iterations
                  • Update-variable-value
                  • Exec-unary
                  • Values+denv
                  • Init-vcscope-dinfo-loop
                  • Extend-denv-with-structdecl
                  • Exec-var/const
                  • Valuemap+denv
                  • Namevalue+denv
                  • Extend-denv-with-fundecl
                  • Ensure-boolean
                  • Int+denv
                  • Push-vcscope-dinfo
                  • Extend-denv-with-topdecl-list
                  • Exec-literal
                  • Build-denv-from-file
                  • Namevalue+denv-result
                  • Extend-denv-with-topdecl
                  • Evalue+denv-result
                  • Value?+denv-result
                  • Values+denv-result
                  • Valuemap+denv-result
                  • Int+denv-result
                  • Push-call-dinfo
                  • Exec-print
                  • Pop-vcscope-dinfo
                  • Exec-if
                  • Exec-function
                  • Pop-call-dinfo
                  • Exec-statement-list
                  • Exec-block
                  • Exec-struct-init-list
                  • Exec-struct-init
                  • Exec-expression-list
                • Values
                • Dynamic-environments
                • Arithmetic-operations
                • Curve-parameterization
                • Shift-operations
                • Errors
                • Value-expressions
                • Locations
                • Input-execution
                • Edwards-bls12-generator
                • Equality-operations
                • Logical-operations
                • Program-execution
                • Ordering-operations
                • Bitwise-operations
                • Literal-evaluation
                • Type-maps-for-struct-components
                • Output-execution
                • Tuple-operations
                • Struct-operations
              • 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
  • Execution

Evalue+denv

Fixtype of pairs consisting of an expression value and a dynamic environment.

This is a product type introduced by fty::defprod.

Fields
evalue — expr-value
denv — denv

In general, the execution of an expression not only yields an expression value (see expr-value, but also affects the dynamic environment. Actually, this is not quite the case in the current simple version of Leo, but it will likely be the case when Leo is extended; so we formalize the necessary mathematical structure for right now.

Subtopics

Evalue+denv-fix
Fixing function for evalue+denv structures.
Evalue+denv-equiv
Basic equivalence relation for evalue+denv structures.
Make-evalue+denv
Basic constructor macro for evalue+denv structures.
Evalue+denv->evalue
Get the evalue field from a evalue+denv.
Evalue+denv->denv
Get the denv field from a evalue+denv.
Change-evalue+denv
Modifying constructor for evalue+denv structures.
Evalue+denv-p
Recognizer for evalue+denv structures.