• 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
            • Constraint-fix
            • Constraint-case
            • Constraintp
            • Constraint-equiv
            • Constraint-relation
            • Constraint-equal
            • Constraint-kind
          • Definition-option
          • Abstract-syntax-operations
          • System
          • Convenience-constructors
          • 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

Constraint

Fixtype of constraints.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:equal → constraint-equal
:relation → constraint-relation

A constraint is either an equality of expressions, or the application of a named relation to argument expressions. We use (any) strings for relation names.

In the future, this may be extended with propositional connectives to combine equalities and applications of named relations.

Subtopics

Constraint-fix
Fixing function for constraint structures.
Constraint-case
Case macro for the different kinds of constraint structures.
Constraintp
Recognizer for constraint structures.
Constraint-equiv
Basic equivalence relation for constraint structures.
Constraint-relation
Constraint-equal
Constraint-kind
Get the kind (tag) of a constraint structure.