--- Day changed Thu Apr 13 2017
comieteksubttle: I don't know about fibres, but I did find myself needing the max element of a Fin13/04 07:27
comieteksubttle: https://gist.github.com/mietek/bb5e152660c12abf1b59a69aab5d4f0f13/04 07:38
quchenI’m getting a strange error when trying to declare {-# BUILTIN NATEQUALS _==_ #-}. I have (_≟_ : Decidable {A = ℕ} _≡_), so (x == y = ⌊ x ≟ y ⌋) ought to be a valid definition for equality of Nats, no?13/04 08:12
quchenYet Agda complains that »succ n != n of type ℕ when checking the pragma BUILTING NATEQUALS _==_«13/04 08:12
quchenAnother question: other than for scoping across all constructors, is there any reason to put parameters in data definitions on the left-hand side of the »:«?13/04 08:25
quchene.g. data Vector : (A : Set) -> Nat -> A -> Set where …13/04 08:26
quchen… instead of data Vector (A : Set) : Nat -> Set where …13/04 08:26
gallaisquchen: if you put it on the right hand side, it's an index. You'll have to store it in the constructors and the type's level will be bumped by one because of that13/04 09:10
quchenLevel?13/04 09:10
quchenYou mean I’ll get a Set1 because of doing something like this?13/04 09:11
quchenSo my Vector : (A : Set) … will be a Set-1, not a Set?13/04 09:11
quchengallais: 13/04 09:12
gallaisyes13/04 09:27
quchenHm. Then I guess I don’t understand levels anymore.13/04 09:30
quchenSo far, my mental model was »types that contain other types must be at higher levels than what they contain«13/04 09:30
quchenBut (Vector {l} (A : Set l) : Nat -> Set l where …) defines a vector that has the same level as its contents13/04 09:31
quchenThis is exactly what you mentioned, yes, but still it confuses me why this is different to putting the parameter on the RHS of the :13/04 09:32
comietekquchen: e.g. https://ziman.functor.sk/oldblog/index.html%3Fp=443.html13/04 10:25
comietekhttp://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices13/04 10:26
comietekhttps://www.quora.com/What-is-different-between-a-parameter-and-an-index-to-a-type13/04 10:26
comietekhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Data13/04 10:26
quchenOkay okay :-)13/04 10:33
quchenThanks!13/04 10:33
quchenI’ve read some of them, but it didn’t click yet.13/04 10:33
quchenReading it again might help maybe.13/04 10:33
quchenGut feeling improved, but not crystal clear. So far, so good. :-)13/04 10:42
quchenUp next: »rewrite«. I know what it desugars to, which brings me to that I don’t understand unification very well either.13/04 10:42
quchenIt’s easy to imagine that using x ≡ y allows me to replace all x with y.13/04 10:43
quchenBut Agda is much more powerful: it also works for whole expressions, like succ x = succ (succ y).13/04 10:43
quchenWhen I rewrite using that, it feels like I’m instructing Agda to find all subexpressions containing succ x and performing the substitution on them.13/04 10:44
quchenIn other words, I feel like rewrite magically finds all places where one could apply the rewrite.13/04 10:44
quchenFWIW, the desugaring I know is from http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching13/04 10:47
quchen  f ps rewrite eqn = rhs13/04 10:47
quchen>>>>>13/04 10:47
quchen  f ps with a | eqn13/04 10:47
quchen  … | ._ | refl = rhs13/04 10:47
quchenWhat’s the match on »a« for if all we do is ignore it? Assert that it’s matchable?13/04 10:48
--- Log closed Thu Apr 13 16:06:15 2017
--- Log opened Thu Apr 13 16:08:26 2017
-!- Irssi: #agda: Total of 139 nicks [0 ops, 0 halfops, 0 voices, 139 normal]13/04 16:08
-!- Irssi: Join to #agda was synced in 161 secs13/04 16:11
subttlecomietek: thank you!13/04 16:40
subttlecomietek: I have class now but I will take a look tonight13/04 20:57

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