aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 11 Pull Requests 1 Packages Projects Releases Wiki Activity

doc: Not call out LeanDojo

This commit is contained in:
Leni Aniva 2024-10-24 22:51:26 -07:00 committed by Leni Aniva
parent e1d27d6ae0
commit a61cea3a2f
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
docs/intro.md
View File

@ -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 authors, this is a mistake. An interface conducive for human operators to write
proofs is often not an interface conductive to search. proofs is often not an interface conductive to search.
LeanDojo has architectural limitations that prevent it from gaining new features Almost all of Pantograph's business logic is written in Lean, and Pantograph
such as drafting without refactoring. Almost all of Pantograph's business logic achieves tighter coupling between the data extraction and proof search
is written in Lean, and Pantograph achieves tighter coupling between the data components.
extraction and proof search components.
## Referencing ## Referencing