• 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
                  • Abs-*-hexadecimal-digit-to-nat
                  • Abs-*-decimal-digit-to-nat
                  • Chars+exprs
                    • Chars+exprs-fix
                    • Chars+exprs-equiv
                    • Make-chars+exprs
                    • Chars+exprs->exprs
                    • Chars+exprs->chars
                    • Change-chars+exprs
                    • Chars+exprs-p
                  • Abs-transition-declaration
                  • Abs-not-double-quote-or-backslash-or-line-feed-or-carriage-return
                  • Abs-named-type
                  • Chars+exprs-result
                  • Abs-*-lowercaseletter/decimaldigit
                  • Abs-*-letter/decimaldigit/underscore
                  • Abs-*-comma-struct-component-declaration
                  • Abs-hexadecimal-digit-to-nat
                  • Abs-assignment-operator
                  • Abs-struct-component-declarations
                  • Abs-lowercaseletter/decimaldigit
                  • Abs-letter/decimaldigit/underscore
                  • Abs-increment-statement
                  • Abs-group-coordinate
                  • Abs-function-parameter
                  • Abs-function-declaration
                  • Abs-decrement-statement
                  • Abs-unsigned-literal
                  • Abs-record-declaration
                  • Abs-mapping-declaration
                  • Abs-variable-declaration
                  • Abs-signed-literal
                  • Abs-constant-declaration
                  • Abs-*-comma-function-parameter
                  • Abs-unicode-character-escape
                  • Abs-struct-declaration
                  • Abs-struct-component-declaration
                  • Abs-simple-character-escape
                  • Abs-finalizer
                  • Abs-decimal-digit-to-nat
                  • Abs-comma-struct-component-declaration
                  • Abs-affine-group-literal
                  • Check-literal-is-string-literal
                  • Abs-*-annotation
                  • Abs-variable-or-free-constant
                  • Abs-string-literal-element
                  • Abs-program-item
                  • Abs-program-declaration
                  • Abs-print-arguments
                  • Abs-octal-digit-to-nat
                  • Abs-finalize-statement
                  • Abs-declaration
                  • Abs-decimal-digit-to-char
                  • Abs-console-statement
                  • Abs-assignment-statement
                  • Abs-ascii-character-escape
                  • *binary-opcall-name-to-binop*
                  • Abs-?-function-parameters
                  • Abs-*-string-literal-element
                  • Abs-*-import-declaration
                  • Abs-uppercase-letter
                  • Abs-unsigned-type
                  • Abs-signed-type
                  • Abs-return-statement
                  • Abs-product-group-literal
                  • Abs-print-call
                  • Abs-named-primitive-type
                  • Abs-lowercase-letter
                  • Abs-import-declaration
                  • Abs-identifier
                  • Abs-function-parameters
                  • Abs-comma-function-parameter
                  • Abs-?-output-type
                  • Abs-*-declaration
                  • Abs-unit-expression
                  • Abs-string-literal
                  • Abs-program-id
                  • Abs-numeric-literal
                  • Abs-letter
                  • Abs-integer-literal
                  • Abs-double-quote-escape
                  • Abs-carriage-return-escape
                  • Abs-boolean-literal
                  • Abs-atomic-literal
                  • Abs-assert-call
                  • Abs-arithmetic-type
                  • Abs-address-literal
                  • Check-optional-equals-p
                  • Abs-?-finalizer
                  • Abs-*-program-item
                  • Abs-scalar-literal
                  • Abs-null-character-escape
                  • Abs-locator
                  • Abs-integer-type
                  • Abs-horizontal-tab-escape
                  • Abs-field-literal
                  • Abs-console-call
                  • Abs-backslash-escape
                  • Abs-annotation
                  • Check-?-comma
                  • Abs-unit-type
                  • Abs-string-type
                  • Abs-scalar-type
                  • Abs-literal
                  • Abs-line-feed-escape
                  • Abs-double-quote
                  • Abs-boolean-type
                  • Abs-address-type
                  • Empty-optional-tree-p
                  • Abs-numeral
                  • Abs-group-type
                  • Abs-file
                  • Abs-field-type
                  • Unop-for-opcall-name
                  • Binop-for-opcall-name
                  • Abs-safe-nonascii
                  • *unary-opcall-name-to-unop*
                  • Abs-?-expression-*-comma-expression-?-comma
                  • Abs-*-comma-struct-component-initializer
                  • Abs-1*-comma-expression
                  • Abs-*-statement
                  • Abs-*-comma-type
                  • Abs-*-comma-expression
                  • Abs-unary-operator-call
                  • Abs-unary-expression
                  • Abs-tuple-expression
                  • Abs-tuple-component-expression
                  • Abs-struct-expression
                  • Abs-struct-component-initializer
                  • Abs-struct-component-expression
                  • Abs-shift-expression
                  • Abs-primary-expression
                  • Abs-postfix-expression
                  • Abs-ordering-expression
                  • Abs-multiplicative-expression
                  • Abs-function-arguments
                  • Abs-free-function-call
                  • Abs-exponential-expression
                  • Abs-exclusive-disjunctive-expression
                  • Abs-equality-expression
                  • Abs-disjunctive-expression
                  • Abs-conjunctive-expression
                  • Abs-conditional-ternary-expression
                  • Abs-conditional-statement
                  • Abs-conditional-disjunctive-expression
                  • Abs-conditional-conjunctive-expression
                  • Abs-comma-struct-component-initializer
                  • Abs-comma-expression
                  • Abs-block
                  • Abs-binary-operator-call
                  • Abs-binary-expression
                  • Abs-additive-expression
                  • Abs-1*-comma-type
                  • Abs-type
                  • Abs-tuple-type
                  • Abs-statement
                  • Abs-operator-call
                  • Abs-loop-statement
                  • Abs-expression
                  • Abs-comma-type
                  • Abs-branch
                • Statement
                • Files
                • Input-files
                • 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
  • Syntax-abstraction

Chars+exprs

Fixtype of pairs consisting of a list of Leo characters and a list of expressions.

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

Fields
chars — char-list
exprs — expression-list

Subtopics

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