From a61cea3a2f0905c85539782a6388f58ac4949d84 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 24 Oct 2024 22:51:26 -0700 Subject: [PATCH] doc: Not call out LeanDojo --- docs/intro.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/intro.md b/docs/intro.md index 9d31f1c..c7ef45a 100644 --- a/docs/intro.md +++ b/docs/intro.md @@ -19,10 +19,9 @@ know that the Coq Serapi was superseded by CoqLSP. In the opinion of the authors, this is a mistake. An interface conducive for human operators to write proofs is often not an interface conductive to search. -LeanDojo has architectural limitations that prevent it from gaining new features -such as drafting without refactoring. Almost all of Pantograph's business logic -is written in Lean, and Pantograph achieves tighter coupling between the data -extraction and proof search components. +Almost all of Pantograph's business logic is written in Lean, and Pantograph +achieves tighter coupling between the data extraction and proof search +components. ## Referencing