From e3e38ec219e223a2f850c6288eb7180edac1856a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 15 Jan 2024 07:56:48 +0100 Subject: [PATCH] wip --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 25b11df7..7e9e341f 100644 --- a/README.md +++ b/README.md @@ -26,8 +26,8 @@ formalizing the metatheory of first-order logic can be exported and translated to Dedukti, Lambdapi and Coq in a few minutes. However, it may take hours for Coq and require too much memory for Lambdapi to check the translated files. Bigger libraries like -`Multivariate/make.ml` requires too much memory for the moment. But we -will fix this soon. +`Multivariate/make.ml` requires too much memory for the moment. We +hope to fix this soon. Moreover, while it is possible to translate any HOL-Light proof to Coq, the translated theorem may not be directly usable by Coq users