• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Semantics
        • Lifting
        • R1cs-subset
        • Well-formedness
        • Abstract-syntax
          • Syntax-abstraction
          • Abstract-syntax-trees
          • Abstract-syntax-operations
          • Convenience-constructors
            • Constraint/constraintlist-p
            • Pfdef
            • Constraint/constraintlist-listp
            • Pfname
            • Yyyjoin
            • Pf+
            • Pf*
            • Pfnames
            • Pfmon
            • Pf=
            • Pfconst
            • Pfcall
            • Pfvar
        • 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
      • Riscv
      • 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
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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.
Pfname
Construct a name.
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.
Pfnames
Construct a list of indexed names.
Pfmon
Construct a monomial, i.e. a product of a constant by a variable, from an integer and a name.
Pf=
Construct an equality constraint.
Pfconst
Construct a constant expression from an integer.
Pfcall
Construct a relation call constraint.
Pfvar
Construct a variable expression from a name.