• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
        • Lp-section-8
        • Lp-section-10
        • Lp-section-6
        • Lp-section-9
        • Lp-section-17
        • Lp-section-16
        • Lp-section-15
        • Lp-section-11
        • Lp-section-4
        • Lp-section-7
        • Lp-section-13
        • Lp-section-12
        • Lp-section-14
        • Lp-section-5
        • Lp-section-0
        • Lp-section-2
        • Lp-section-18
        • Lp-section-3
        • Lp-section-1
      • Fast-alists
      • Defconst
      • Defmacro
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Loop$-primer

Lp-section-0

Loop$ Primer Table of Contents)

The Loop$ Primer Table of Contents

• loop$-primer:   Preface
  
• lp-section-0:   Table of Contents
  
• lp-section-1:   Background Reviews
  
• lp-section-2:   Loop in Common Lisp and loop$ in ACL2
  
• lp-section-3:   Examples of FOR Loop$s
  
• lp-section-4:   Syntax of FOR Loop$s
  
• lp-section-5:   Informal Semantics of FOR Loop$s
  
• lp-section-6:   Challenge Problems about FOR Loop$s
  
• lp-section-7:   Using Loop$s and Guards in Defuns
  
• lp-section-8:   Challenge Problems about FOR Loop$ in Defuns
  
• lp-section-9:   Semantics of FOR Loop$s
  
• lp-section-10: The Evaluation of the Formal Semantics of a Fancy Loop$
  
• lp-section-11: Proving Theorems about FOR Loop$s
  
• lp-section-12: Challenge Proof Problems about FOR Loop$s
  
• lp-section-13: Examples of DO Loop$s
  
• lp-section-14: Challenge Problems about DO Loop$s
  
• lp-section-15: Informal Syntax and Semantics of DO Loop$s
  
• lp-section-16: Proving Theorems about DO Loop$s
  
• lp-section-17: Challenge Proof Problems for DO Loop$s
  
• lp-section-18: Conclusion
  
• lp-section-0:   Table of Contents