diff --git a/src/exercises/02_iff_if_and.lean b/src/exercises/02_iff_if_and.lean index 9980421..29f30b6 100644 --- a/src/exercises/02_iff_if_and.lean +++ b/src/exercises/02_iff_if_and.lean @@ -340,8 +340,9 @@ end /- Of course using `split` only to be able to use `exact` twice in a row feels silly. One can also use the anonymous constructor syntax: ⟨ ⟩ -Beware those are not parentheses but angle brackets. This is a generic way of providing -compound objects to Lean when Lean already has a very clear idea of what it is waiting for. +Beware those are not parentheses but angle brackets. You can type them as \< and \> in VS +Code. They are a generic way of providing compound objects to Lean when Lean already has a +very clear idea of what it is waiting for. So we could have replaced the last three lines by: exact ⟨hQ, hP⟩ diff --git a/src/solutions/02_iff_if_and.lean b/src/solutions/02_iff_if_and.lean index 6990ffb..6c09bd8 100644 --- a/src/solutions/02_iff_if_and.lean +++ b/src/solutions/02_iff_if_and.lean @@ -391,8 +391,9 @@ end /- Of course using `split` only to be able to use `exact` twice in a row feels silly. One can also use the anonymous constructor syntax: ⟨ ⟩ -Beware those are not parentheses but angle brackets. This is a generic way of providing -compound objects to Lean when Lean already has a very clear idea of what it is waiting for. +Beware those are not parentheses but angle brackets. You can type them as \< and \> in VS +Code. They are a generic way of providing compound objects to Lean when Lean already has a +very clear idea of what it is waiting for. So we could have replaced the last three lines by: exact ⟨hQ, hP⟩