--- Day changed Mon Apr 10 2017
subttleI ran into another internal error, I think it's just parsing @ 10/04 00:11
subttleAn internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Rules/LHS.hs:49610/04 00:11
subttlehappened when I forgot to add parentheses when naming & deconstructing, I can file a ticket in a bit10/04 00:12
subttleas in list@(h :: t)10/04 00:12
subttleI get an internal error for list@h :: t10/04 00:13
rntzis there a good guide on how to use the "syntax" declaration on agda somewhere?10/04 00:14
subttlealso, on an unrelated note, I made an obvious minor typo yesterday in my question, I forgot to make `d` a singleton10/04 00:14
rntzI'm trying to make it so that "\exists[ x \in A ] B" turns into "\exists (\lambda x -> x \in A \x B)"10/04 00:15
rntz(where I've defined an _\in_ operator already)10/04 00:15
rntzbut I am getting rather mystifying error messages10/04 00:15
subttleoh and this is for Agda 2.5.210/04 00:26
subttleI've narrowed it down to a small snippet. If anyone could test if this is reproducible, I will file the bug report right now... using agda-stdlib 0.1310/04 00:58
lpastesubttle pasted “Internal error parsing as-pattern” at http://lpaste.net/35446810/04 00:59
subttlehttps://github.com/agda/agda/issues/253810/04 01:03
mieteksubttle: yes10/04 03:29
mieteksubttle: still around?10/04 03:29
subttlemietek: thanks!10/04 03:29
mieteksorry, I haven’t tried reproducing it10/04 03:30
mieteksubttle: I just mean I know how to use "syntax" declarations10/04 03:30
subttleoh do you mean rntz? :)10/04 03:30
mietekerr10/04 03:30
mietekI do.10/04 03:30
mieteksorry.10/04 03:30
subttleno worries!10/04 03:31
mieteksubttle: @-patterns are quite new10/04 03:31
mietekI think it’s likely that they contain bugs10/04 03:31
subttlemietek: ah, I see10/04 03:31
mietekrntz: still around?10/04 03:31
mietekrntz: a good thing to remember is that https://agda.github.io/agda-stdlib/Data.Product.html#1 contains a syntax declaration10/04 03:32
mietekrntz: syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B10/04 03:32
mietekrntz: the LHS must include a target symbol (here "Σ-syntax"), which must not contain "_" characters10/04 03:34
mietekrntz: each variable bound on the LHS must be used on the RHS, I think…10/04 03:35
mietekrntz: and each use on the RHS must be separated from any other use by at least one boilerplate character10/04 03:35
mietekrntz: however, partial application still works, so there is some flexibility to be gained by not binding every possible variable10/04 03:36
mietekrntz: the one situation in which a syntax declaration is irreplaceable is when you want to switch around the order of dependent arguments10/04 03:38
mietekrntz: e.g. "syntax ≡→Eq⟨…⟩ {A} u p p′ = u ≡→Eq⟨ A ⟩⟨ p ⟩ p′"10/04 03:39
akr[m]any tips on how to define something like a multiset in agda, but so that I can actually modify it easily?10/04 09:36
akr[m]i.e. if I have a multiset where there are n copies of A, I'd like to be easily able to create a new multiset where there are n+1 copies of n10/04 09:37
akr[m]of A*10/04 09:37
akr[m]defining it like an abstract record doesn't seem to be the best way10/04 09:38
akr[m]also I know the carrier is always finite10/04 09:38
akr[m]so ideally I should be able to compute with these at least somewhat conveniently10/04 09:39
akr[m]e.g. if I have n copies of A, inserting another A also gives me a proof that now I have n+1 copies of it10/04 09:40
gallaisakr[m]: if your type has a total order on it, ordered list yield a canonical representation of multisets10/04 09:40
gallaisalternatively, strictly ordered lists of pairs of a non-zero nat and an element also work10/04 09:41
akr[m]gallais: I considered using plain lists, what advantages would ordered lists give me?10/04 09:42
Caleakr[m]: Well, it would give you the property that if xs = ys then they represent the same multiset.10/04 09:48
CaleI wonder if anyone's implemented something like Haskell's Data.Map (and then proven a bunch of theorems about it)10/04 09:49
akr[m]ah yeah I guess that could be quite useful10/04 09:59
akr[m]something like Data.Map could be nice as well… I mean, I'm imagining that's what you pretty much end up writing anyway10/04 10:00
gallaisakr[m]: https://agda.github.io/agda-stdlib/Data.AVL.html#110/04 10:27
akr[m]gallais: interesting10/04 10:32
akr[m]so I don't really care about performance10/04 10:34
akr[m]I mostly want something that's easy to work with10/04 10:34
akr[m]what should I use?10/04 10:34
akr[m]also it might be annoying to have to construct a linear order on my type10/04 10:35
akr[m]total order*10/04 10:36
apostolisHello, will typechecking times improve with a multicore cpu or does performance per core is more important?10/04 22:56

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