From 51477a48068de0e39f26928130c56414c9934786 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 May 2023 19:12:07 -0700 Subject: [PATCH] Remove testing stub in README.md --- README.md | 9 --------- 1 file changed, 9 deletions(-) diff --git a/README.md b/README.md index 617552d..13a0f3d 100644 --- a/README.md +++ b/README.md @@ -57,15 +57,6 @@ proof.printTree {"treeId": 0} ``` where the application of `assumption` should lead to a failure. -``` -create {"imports": ["Init"]} -proof.start {"id": 0, "expr": "∀ (p q: Prop), p ∨ q → q ∨ p"} -proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro p q h"} -proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "cases h"} -proof.tactic {"treeId": 0, "stateId": 2, "goalId": 0, "tactic": "apply Or.inr"} -proof.tactic {"treeId": 0, "stateId": 2, "goalId": 0, "tactic": "apply Or.inl"} -``` - ## Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: