• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
        • Fgl-rewrite-rules
          • Binder-functions
          • Fgl-syntactic-checker-binders
          • Binder
          • Fancy-ev
          • Binder-rules
          • Def-fgl-program
          • Bind-var
          • Add-fgl-brewrites
          • Def-fgl-rewrite
          • Narrow-equiv
          • Def-fgl-branch-merge
          • Add-fgl-rewrites
          • Fgl-interp-obj
          • Syntax-bind
          • Collect-cmr-rewrites-for-formula-name
          • Fgl-time
          • Fgl-prog2
          • Assume
          • Add-fgl-binder-meta
          • Add-fgl-primitive
          • Add-fgl-meta
          • Add-fgl-branch-merges
          • Cmr::rewritelist->lhses
          • Remove-fgl-brewrites
          • Remove-fgl-branch-merges
          • Lhses->branch-function-syms
          • Enable-execution
          • Abort-rewrite
          • Syntax-interp
            • Remove-fgl-rewrites
            • Lhses->leading-function-syms
            • Remove-fgl-primitive
            • Remove-fgl-binder-meta
            • If!
            • Disable-execution
            • Remove-fgl-meta
            • Fgl-time-fn
            • Disable-definition
            • Def-fgl-brewrite
          • Fgl-function-mode
          • Fgl-object
          • Fgl-solving
          • Fgl-handling-if-then-elses
          • Fgl-getting-bits-from-objects
          • Fgl-primitive-and-meta-rules
          • Fgl-counterexamples
          • Fgl-interpreter-overview
          • Fgl-correctness-of-binding-free-variables
          • Fgl-debugging
          • Fgl-testbenches
          • Def-fgl-boolean-constraint
          • Fgl-stack
          • Fgl-rewrite-tracing
          • Def-fgl-param-thm
          • Def-fgl-thm
          • Fgl-fast-alist-support
          • Fgl-array-support
          • Advanced-equivalence-checking-with-fgl
          • Fgl-fty-support
          • Fgl-internals
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Fgl-rewrite-rules

    Syntax-interp

    Interpret a form on the syntactic representations of variables.

    Logically, this always returns NIL. In FGL, this can be used when under an unequiv congruence to examine the syntactic representation of certain values and also to access and update the ACL2 state and FGL interpreter state.