|
|
|---|
|
|
|
|---|
An introductory guide, recommended for new users of gl.
This is a tutorial introduction to using GL to prove ACL2 theorems. We recommend going through the entire tutorial before beginning to use GL.
You can think of this tutorial as a quick-start guide. By the time you're done with it, you should have a good understanding of how GL works, and be able to use GL to easily prove many theorems.
We don't try to cover more advanced topics, like optimization and term-level-reasoning. You'll probably want to get some practice using GL before exploring these topics.