avigad
commented
5 years ago Good catch! I'll add the word "also", since the net result is that alpha and beta are both implicit in both constructors. Thanks for the fix and for the kind words.
Closed marcusklaas closed 5 years ago
avigad
commented
5 years ago Good catch! I'll add the word "also", since the net result is that alpha and beta are both implicit in both constructors. Thanks for the fix and for the kind words.
I am very new to lean, so I hope this is right. The usage of α and β seem to be swapped at this particular line. Very good documentation btw, I've learned a lot!