• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
    • 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
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • 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