• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Abstract-syntax
          • Syntax-abstraction
          • Expression
          • Definition
          • Constraint
          • Definition-option
          • Abstract-syntax-operations
          • System
          • Convenience-constructors
            • Constraint/constraintlist-p
            • Pfdef
            • Constraint/constraintlist-listp
            • Yyyjoin
            • Pf+
            • Pf*
            • Pfmon
            • Pf=
            • Pfcall
            • Pfvar
            • Pfconst
          • System-result
          • Expression-result
          • Expression-list-result
          • Definition-result
          • Definition-list-result
          • Constraint-result
          • Constraint-list-result
          • Expression-list
          • Definition-list
          • Constraint-list
        • R1cs-subset
        • Semantics
        • Abstract-syntax-operations
        • Indexed-names
        • Well-formedness
        • Concrete-syntax
        • R1cs-bridge
        • Parser-interface
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • 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
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-syntax

Convenience-constructors

Utilities to convniently construct PFCS abstract syntax.

These functions and macros have short and evocative names, to support the concise and readable construction of (constituents of) rules in the abstract syntax.

Subtopics

Constraint/constraintlist-p
Recognize constraints and lists of constraints.
Pfdef
Construct a definition with zero or more constraints.
Constraint/constraintlist-listp
Recognize lists of constraints and lists of constraints.
Yyyjoin
Spread a binary function over two or more arguments.
Pf+
Construct an addition of any number of expressions.
Pf*
Construct a multiplication of any number of expressions.
Pfmon
Construct a monomial, i.e. a product of a constant by a variable.
Pf=
Construct an equality constraint.
Pfcall
Construct a relation call constraint.
Pfvar
Construct a variable expression.
Pfconst
Construct a constant expression.