3 ms·

Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom. I love to look at unicode, but is it a pain to type it in practice, eve

• evincarofautumn 12y ago
  I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.
• chas 12y ago
  Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0] [0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...
• tel 12y ago
  Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are. What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like theorem1 : T (1 - 1 == 0) which is somewhat interestingly different from theorem2 : 1 - 1 = 0 in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).