subttle subttle --- Day changed Mon Apr 10 2017 I ran into another internal error, I think it's just parsing @ 10/04 00:11 An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Rules/LHS.hs:496 10/04 00:11 happened when I forgot to add parentheses when naming & deconstructing, I can file a ticket in a bit 10/04 00:12 as in list@(h :: t) 10/04 00:12 I get an internal error for list@h :: t 10/04 00:13 is there a good guide on how to use the "syntax" declaration on agda somewhere? 10/04 00:14 also, on an unrelated note, I made an obvious minor typo yesterday in my question, I forgot to make d a singleton 10/04 00:14 I'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 (where I've defined an _\in_ operator already) 10/04 00:15 but I am getting rather mystifying error messages 10/04 00:15 oh and this is for Agda 2.5.2 10/04 00:26 I'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.13 10/04 00:58 subttle pasted “Internal error parsing as-pattern” at http://lpaste.net/354468 10/04 00:59 https://github.com/agda/agda/issues/2538 10/04 01:03 subttle: yes 10/04 03:29 subttle: still around? 10/04 03:29 mietek: thanks! 10/04 03:29 sorry, I haven’t tried reproducing it 10/04 03:30 subttle: I just mean I know how to use "syntax" declarations 10/04 03:30 oh do you mean rntz? :) 10/04 03:30 err 10/04 03:30 I do. 10/04 03:30 sorry. 10/04 03:30 no worries! 10/04 03:31 subttle: @-patterns are quite new 10/04 03:31 I think it’s likely that they contain bugs 10/04 03:31 mietek: ah, I see 10/04 03:31 rntz: still around? 10/04 03:31 rntz: a good thing to remember is that https://agda.github.io/agda-stdlib/Data.Product.html#1 contains a syntax declaration 10/04 03:32 rntz: syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B 10/04 03:32 rntz: the LHS must include a target symbol (here "Σ-syntax"), which must not contain "_" characters 10/04 03:34 rntz: each variable bound on the LHS must be used on the RHS, I think… 10/04 03:35 rntz: and each use on the RHS must be separated from any other use by at least one boilerplate character 10/04 03:35 rntz: however, partial application still works, so there is some flexibility to be gained by not binding every possible variable 10/04 03:36 rntz: the one situation in which a syntax declaration is irreplaceable is when you want to switch around the order of dependent arguments 10/04 03:38 rntz: e.g. "syntax ≡→Eq⟨…⟩ {A} u p p′ = u ≡→Eq⟨ A ⟩⟨ p ⟩ p′" 10/04 03:39 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 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 n 10/04 09:37 of A* 10/04 09:37 defining it like an abstract record doesn't seem to be the best way 10/04 09:38 also I know the carrier is always finite 10/04 09:38 so ideally I should be able to compute with these at least somewhat conveniently 10/04 09:39 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 it 10/04 09:40 akr[m]: if your type has a total order on it, ordered list yield a canonical representation of multisets 10/04 09:40 alternatively, strictly ordered lists of pairs of a non-zero nat and an element also work 10/04 09:41 gallais: I considered using plain lists, what advantages would ordered lists give me? 10/04 09:42 akr[m]: Well, it would give you the property that if xs = ys then they represent the same multiset. 10/04 09:48 I wonder if anyone's implemented something like Haskell's Data.Map (and then proven a bunch of theorems about it) 10/04 09:49 ah yeah I guess that could be quite useful 10/04 09:59 something like Data.Map could be nice as well… I mean, I'm imagining that's what you pretty much end up writing anyway 10/04 10:00 akr[m]: https://agda.github.io/agda-stdlib/Data.AVL.html#1 10/04 10:27 gallais: interesting 10/04 10:32 so I don't really care about performance 10/04 10:34 I mostly want something that's easy to work with 10/04 10:34 what should I use? 10/04 10:34 also it might be annoying to have to construct a linear order on my type 10/04 10:35 total order* 10/04 10:36 Hello, will typechecking times improve with a multicore cpu or does performance per core is more important? 10/04 22:56