lean4-htt/library/tools
Leonardo de Moura a0a8103804 chore(frontends/lean): go back to 'c' as notation for characters
This suggestion has been discussed at Slack.
We have decided to use #"c" as notation because we wanted to allow `'`
in the beginning of identifiers like in SML and F*. In particular,
we wanted to allow users to use 'a 'b 'c for naming type parameters
like in SML. However, nobody used this notation. In the Lean standard
library, we are using greek letters for naming type parameters.
So, there is no real motivation for the ugly #"c" syntax.
2017-05-02 13:00:51 -07:00
..
debugger chore(frontends/lean): go back to 'c' as notation for characters 2017-05-02 13:00:51 -07:00
mini_crush chore(library/tools/mini_crush/default): increase timeout 2017-04-30 16:27:55 -07:00
super feat(library/init/category): add has_map type class, delete fmap 2017-05-01 10:13:02 -07:00