tomahawkins/ivory-backend-acl2 — pull request #1 by leepike (2014-04-03 17:20:47+00:00)
Title: Small "Hoare" example to test the ACL2 backend.

Small example using 'requires' and 'ensures' constructs.