• 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
            • Abstract-syntax
            • Dynamic-semantics
            • Compilation
            • Static-semantics
              • Type-checking
                • Typecheck-expressions
                • Typecheck-statements
                • Typecheck-expression
                • Typecheck-statement
                • Funparam-list-to-var/const-sinfo-list
                • Typecheck-call
                • Expr-type-list->sort-list
                • Typecheck-binop
                • Expr-type-list->type-list
                • Types+senv
                • Typecheck-literal
                • Typecheck-print-args
                • Expr-sort
                • Typecheck-type
                • Typecheck-fundecl
                • Typecheck-unop
                • Typecheck-constdecl
                • Extend-senv-with-structdecl
                • Typecheck-structdecl
                • Expr-type
                • Typecheck-vardecl
                • Typecheck-statement-list
                • Extend-senv-with-constdecl
                • Typecheck-funparam-list
                • Extend-senv-with-vardecl
                • Extend-senv-with-fundecl
                • Typecheck-compdecl-list
                • Typecheck-funparam
                • Identifier+exprtype
                • Extend-senv-with-topdecl-list
                • Typecheck-console
                • Identifier-exprtype-map-constp
                • Types+senv-result
                • Typecheck-topdecl-list
                • Typecheck-compdecl
                • Identifier+exprtype-result
                • Identifier-exprtype-map-result
                • Funparam-to-var/const-sinfo
                • Extend-senv-with-topdecl
                • Identexprtype-map-to-identype-map
                • Expr-type-result
                • Expr-type-list-result
                • Typecheck-topdecl
                • Typecheck-file
                • Typecheck-branch-list
                • File-to-senv
                • Identifier-exprtype-map
                • Typecheck-struct-init
                • Typecheck-branch
                • Expr-type-list
                • Expr-sort-list
                  • Expr-sort-list-fix
                  • Expr-sort-list-equiv
                  • Expr-sort-listp
                • Typecheck-expression-list
              • Static-environments
              • Curve-parameterization
              • Function-recursion
              • Struct-recursion
              • Input-checking
              • Program-checking
              • Type-maps-for-struct-components
              • Program-and-input-checking
              • Output-checking
            • 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

• Type-checking

Expr-sort-list

Fixtype of lists of expression sorts

This is an ordinary fty::deflist.

Subtopics

Expr-sort-list-fix

(expr-sort-list-fix x) is a usual ACL2::fty list fixing function.

Expr-sort-list-equiv

Basic equivalence relation for expr-sort-list structures.

Expr-sort-listp

(expr-sort-listp x) recognizes lists where every element satisfies expr-sortp.