remove compute tactic from example
commita20abcb06c6f9034f4d29926494f9005a6b6f7c1
authormartinbaker <git29f185@martinb.com>
dateFri 21 Jun 2019, 18:53 (7 years ago)
parent162e468
docs/proofs/interactive.rst−1
@@ -237,7 +237,6 @@ which is trivially provable using reflexivity:
237237 Proof completed!
238238 Main.plusredZ_S = %runElab (do intro `{{k}}
239239 intro `{{ih}}
240− compute
241240 rewriteWith (Var `{{ih}})
242241 reflexivity)
243242