• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
          • Process-syntheto-toplevel-fn
          • Translation
          • Language
            • Static-semantics
              • Check-expression-fns
              • Subtypep
              • Match-type
              • Check-product-update-expression
              • Get-builtin-function-in/out/pre-post
              • Check-sum-update-expression
              • Check-sum-field-expression
              • Check-strict-binary-expression
              • Check-lt/le/gt/ge-expression
              • Check-eq/ne-expression
              • Check-div/rem-expression
              • Check-add/sub/mul-expression
              • Align-let-vars-values
              • Check-iff-expression
              • Check-function-definition-top/nontop
              • Check-sum-construct-expression
              • Check-rem-expression
              • Check-mul-expression
              • Check-sub-expression
              • Check-div-expression
              • Check-add-expression
              • Check-ne-expression
              • Check-lt-expression
              • Check-le-expression
              • Check-gt-expression
              • Check-ge-expression
              • Check-eq-expression
              • Check-function-specifier
              • Type-result
              • Check-product-construct-expression
              • Supremum-type
              • Check-call-expression
              • Check-product-field-expression
              • Check-function-definer
              • Make-subproof-obligations
              • Get-function-in/out/pre/post
              • Check-sum-test-expression
              • Match-field
              • Decompose-expression
              • Match-to-target
              • Check-unary-expression
              • Max-supertype
              • Match-type-list
              • Check-minus-expression
              • Check-type-definition
              • Check-not-expression
              • Check-type-product
              • Match-field-list
              • Check-type-subset
              • Check-type-definition-in-recursion
              • Align-let-vars-values-aux
              • Non-trivial-proof-obligation
              • Check-type-recursion
              • Check-function-specification
              • Check-toplevel
              • Supremum-type-list
              • Check-component-expression
              • Check-branch-list
              • Check-function-recursion
              • Check-function-definition
              • Binding
                • Binding-fix
                • Binding-equiv
                • Make-binding
                • Binding->variables
                • Change-binding
                • Binding->value
                • Bindingp
              • Check-function-header
              • Check-function-definition-list
              • Check-type-definition-list-in-recursion
              • Check-theorem
              • Check-nonstrict-binary-expression
              • Context-add-variables
              • Decompose-expression-aux
              • Check-alternative
              • Check-multi-expression
              • Check-type-sum
              • Check-type
              • Check-alternative-list
              • Context-add-condition
              • Check-type-definer
              • Check-transform
              • Check-variable
              • Check-transform-args
              • Check-toplevel-list
              • Context-add-condition-list
              • Check-if/when/unless-expression
              • Initializers-to-variable-substitution
              • Context-add-binding
              • Check-function-header-list
              • Context-add-toplevel
              • Ensure-single-type
              • Max-supertypes
              • Check-bind-expression
              • Check-type-list
              • Check-literal
              • Literal-type
              • Check-expression-list
              • Variable-context
              • Check-cond-expression
              • Check-branch
              • Args-without-defaults
              • Check-expression
              • *builtin-function-names*
              • Function-called-in
            • Abstract-syntax
            • Outcome
            • Abstract-syntax-operations
            • Outcome-list
            • Outcomes
          • Process-syntheto-toplevel
          • Shallow-embedding
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Static-semantics

Binding

Fixtype of bindings.

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

Fields
variables — typed-variable-list
value — expression

We plan to incorporate this into the abstract syntax, but for now we define this here because we need this to define the static semantics of Syntheto. In particular, as we traverse an expression to check that it satisfies the constraints of the static semantic, we collect the let bindings along the way. This fixtype captures one of these let bindings: it corresponds to the first two components of a binding expression in the abstract syntax.

Subtopics

Binding-fix
Fixing function for binding structures.
Binding-equiv
Basic equivalence relation for binding structures.
Make-binding
Basic constructor macro for binding structures.
Binding->variables
Get the variables field from a binding.
Change-binding
Modifying constructor for binding structures.
Binding->value
Get the value field from a binding.
Bindingp
Recognizer for binding structures.