EECS 755

Software Requirements Modeling and Analysis



PolyList.v is another definition of list that is polymorphic over the type of the list contents. It is a rewrite of Natlist.v with the list type parameterized over content type. All proofs and definitions are re-done.

For your reading enjoyment I’ve also added some basic LTac definitions that take advantage of Coq’s proof scripting capability. LTac is a powerful language for writing tactics and reusing proofs. IN this example I use it to automate induction proofs. I also use autorewrite and rewrite databases to automate some mundane rewriting tasks.