/home/laney/.irssi/irclogs/Freenode/#agda.log-20170303

--- Day changed Thu Mar 02 2017
subttleIs is possible to query the unicode characters in Atom? As with C-u C-x in Emacs? The recent unicode changes have me all discombobulated without it..02/03 21:36
subttleI ask because I don't see it here https://github.com/banacorn/agda-mode02/03 21:38
subttleoops, I meant "C-u C-x ="02/03 22:16
subttleHm, can't seem to find out what \. is now02/03 22:16
subttle\. seems to work in Emacs but not in Atom... weird02/03 22:19
Ptivalhey, what's Agda's syntax for Pi and is there syntax for first-class type annotation?02/03 22:41
rntzPtival: "(a : A) -> B a" is Pi(a : A) B a02/03 22:43
rntzPtival: and I don't know what you mean by first-class type annotation, but I'm guessing no?02/03 22:43
Ptivalsomething like Haskell's `t :: T`, or Coq's `t : T`, as a valid term02/03 22:44
rntzoh, hm, I don't know02/03 22:44
rntzyou can do (let x : T in x), but I don't know whether there's a more direct way02/03 22:45
Ptivalit creates an ambiguity when you have the two with the same syntax02/03 22:45
rntzer, (let x : T; x = whatever in x)02/03 22:45
PtivalI was trying to see what other languages do to deal with this :)02/03 22:45
Ptivalthanks!02/03 22:45
Ptival(you also need `a -> b` for the ambiguity)02/03 22:46
rntzhm?02/03 22:46
Ptivalthat is, if you have `t -> t`, `(t)`, `t : t` and `(t : t) -> t` as four syntactic constructs02/03 22:48
Ptivalthen `(t : t) -> t` could mean either the latter, or a combination of the first three02/03 22:48
Ptivalwith different intent02/03 22:48
rntzah, yeah.02/03 22:48
PtivalI think the least-surprising solution is to make type-annotation look different (or not be first-class)02/03 22:49
Ptivalit's a bit unfortunate :)02/03 22:50
glguyThe stdlib offers _∋_ : ∀ {a} (A : Set a) → A → A; A ∋ x = x02/03 23:23
glguyIn the Function module for type signatures02/03 23:24
Ptivalcool02/03 23:39

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!