2 Commits

Author	SHA1	Message	Date
Adam C. Foltzer	46bcc188f4	fix external bindings not being in scope in let bodies ... The renamer was being run on let bindings without including the NamingEnv of the overall module context. Fixed and added a test case for this.	2014-08-20 11:18:26 -07:00
Adam C. Foltzer	b78062eafe	bind it even when no counterexample/sat is available; add tests ... Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl.	2014-08-19 17:11:43 -07:00