• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
    • Break-rewrite
    • Proof-builder
    • Accumulated-persistence
    • Cgen
      • Defdata
      • Test?
      • ACL2s-defaults
      • Prove/cgen
      • Register-type
      • With-timeout
      • Defdata-attach
      • Testing-enabled
      • Defdata-aliasing-enabled
      • Cgen-single-test-timeout
      • Verbosity-level
      • Search-strategy
      • Num-print-counterexamples
      • Cgen-timeout
      • Cgen-local-timeout
      • Num-witnesses
      • Num-trials
      • Num-print-witnesses
      • Test-then-skip-proofs
      • Sampling-method
      • Recursively-fix
      • Num-counterexamples
      • Backtrack-limit
      • Print-cgen-summary
      • Cgen::flush
      • Backtrack-bad-generalizations
      • Use-fixers
      • Thm-no-test
      • Defthmd-no-test
      • Defthm-no-test
    • Forward-chaining-reports
    • Proof-tree
    • Print-gv
    • Dmr
    • With-brr-data
    • Splitter
    • Guard-debug
    • Set-debugger-enable
    • Redo-flat
    • Time-tracker
    • Set-check-invariant-risk
    • Removable-runes
    • Efficiency
    • Explain-near-miss
    • Tail-biting
    • Failed-forcing
    • Sneaky
    • Invariant-risk
    • Failure
    • Measure-debug
    • Dead-events
    • Compare-objects
    • Prettygoals
    • Remove-hyps
    • Type-prescription-debugging
    • Pstack
    • Trace
    • Set-register-invariant-risk
    • Walkabout
    • Disassemble$
    • Nil-goal
    • Cw-gstack
    • Set-guard-msg
    • Find-lemmas
    • Watch
    • Quick-and-dirty-subsumption-replacement-step
    • Profile-all
    • Profile-ACL2
    • Set-print-gv-defaults
    • Minimal-runes
    • Spacewalk
    • Try-gl-concls
    • Near-misses
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • Cgen
        • Defdata
        • Test?
        • ACL2s-defaults
        • Prove/cgen
        • Register-type
        • With-timeout
        • Defdata-attach
        • Testing-enabled
        • Defdata-aliasing-enabled
        • Cgen-single-test-timeout
        • Verbosity-level
        • Search-strategy
        • Num-print-counterexamples
        • Cgen-timeout
        • Cgen-local-timeout
        • Num-witnesses
        • Num-trials
        • Num-print-witnesses
        • Test-then-skip-proofs
        • Sampling-method
        • Recursively-fix
        • Num-counterexamples
        • Backtrack-limit
        • Print-cgen-summary
        • Cgen::flush
        • Backtrack-bad-generalizations
        • Use-fixers
        • Thm-no-test
        • Defthmd-no-test
        • Defthm-no-test
      • Forward-chaining-reports
      • Proof-tree
      • Print-gv
      • Dmr
      • With-brr-data
      • Splitter
      • Guard-debug
      • Set-debugger-enable
      • Redo-flat
      • Time-tracker
      • Set-check-invariant-risk
      • Removable-runes
      • Efficiency
      • Explain-near-miss
      • Tail-biting
      • Failed-forcing
      • Sneaky
      • Invariant-risk
      • Failure
      • Measure-debug
      • Dead-events
      • Compare-objects
      • Prettygoals
      • Remove-hyps
      • Type-prescription-debugging
      • Pstack
      • Trace
      • Set-register-invariant-risk
      • Walkabout
      • Disassemble$
      • Nil-goal
      • Cw-gstack
      • Set-guard-msg
      • Find-lemmas
      • Watch
      • Quick-and-dirty-subsumption-replacement-step
      • Profile-all
      • Profile-ACL2
      • Set-print-gv-defaults
      • Minimal-runes
      • Spacewalk
      • Try-gl-concls
      • Near-misses
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Cgen
• ACL2s-defaults

Use-fixers

Specify whether fixers are to be used.

By default this parameter is set to nil.

Usage: 
(acl2s-defaults :set use-fixers t) 
(acl2s-defaults :get use-fixers) 
:doc use-fixers