From 2745c174980b8013dcadc527b9a5156b3ad2088e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 17 Jul 2017 14:15:11 +0100 Subject: [PATCH] add some info to known_bugs --- Notes/known_bugs.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Notes/known_bugs.txt b/Notes/known_bugs.txt index e44d1c7..608107b 100644 --- a/Notes/known_bugs.txt +++ b/Notes/known_bugs.txt @@ -1,3 +1,5 @@ +A list of bugs and/or unintuitive behavior in Lean 2: + - 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 @@ -27,5 +29,6 @@ equiv.MK f abstract (* long proof *) end abstract (* long proof *) end ``` +this has the additional advantage that if f and/or g are defined using induction, they will only reduce if they are applied to arguments for which they actually reduce (assuming they have the correct [unfold n] flag. - unfold [foo] also does various (sometimes unwanted) reductions (as if you called esimp)