From 27bd4bc72a26f742a60047c9c92b8403d3c56320 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 30 Mar 2017 16:59:06 -0400 Subject: [PATCH] add file where we keep track of bugs and other undesirable behavior of Lean --- known_bugs.txt | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 known_bugs.txt diff --git a/known_bugs.txt b/known_bugs.txt new file mode 100644 index 0000000..f44968f --- /dev/null +++ b/known_bugs.txt @@ -0,0 +1,27 @@ +- When using the "have" or "assert" tactic, no coercion is applied to the type. So you have to write for example +`have g : Group.carrier G, from _,` +instead of +`have g : G, from _,` + + +- When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`) + + +Issues which are not bugs, but still good to know + +- once you start tactic mode, you cannot specify universe levels anymore + +- esimp is slow, and runs out of memory easily. It is good behavior to split up definitions. So instead of +``` +equiv.MK (* big function *) + (* big inverse *) + (* long proof *) + (* long proof *) +``` +first write the functions f and g and then write +``` +equiv.MK f + g + abstract (* long proof *) end + abstract (* long proof *) end +```