--- Day changed Wed Aug 16 2017
kclancyI'm trying to use sized types, but having some trouble. It seems that there are fragments of my project where the sizes of certain values are irrelevant, and others where it is relevant. After reading the original sized types paper I was under the impression that the inf size could be used where sizes are irrelevant. I keep getting i != inf of type Size errors, though. Maybe I will have to read the new Abel & Puebla paper to understa16/08 00:30
kclancy /away16/08 03:45
Saizan_kclancy: do you have some code examples of this?16/08 09:32
jonsterlingI'm using equational reasoning combinators in Agda, but finding that I would like a version that lets me massage *both sides* of the equation. Does anyone have anything like this?16/08 15:33
Saizan_jonsterling: example?16/08 15:39
mietekjonsterling: eh? you can massage both sides16/08 15:39
jonsterlingmietek: Really, with the equational reasoning combinators? I find that you have to just work one side, at which point if you want to adjust the other side, you have to do it *within* the equality proof 'shed', so everything becomes kind of nested, if that makes any sense.16/08 15:40
mietekbegin sideL ≡⟨ ? ⟩ ... ≡⟨ ? ⟩ sideR ∎16/08 15:40
mietekyes?16/08 15:40
jonsterlingmietek: I think you're misunderstanding my situation, which is fine since I didn't explain it very well...16/08 15:40
mietekpossibly16/08 15:40
jonsterlingIn any case, I have written a combinator to do what I need just now... maybe I will find a better way to do it.16/08 15:40
mietekI was going to say that you can perfectly well go from what I wrote above to both of the following16/08 15:41
mietekbegin sideL ≡⟨⟩ sideL′ ≡⟨ ? ⟩ ... ≡⟨ ? ⟩ sideR ∎16/08 15:41
mietekbegin sideL ≡⟨ ? ⟩ ... ≡⟨ ? ⟩ sideR′ ≡⟨⟩ sideR ∎16/08 15:42
mietek(here using ≡⟨⟩ only for clarity; other transitions work fine, too)16/08 15:42
mietekso, work from both sides of the equation towards a common middle16/08 15:43
mietekwhich is what I thought you want to do16/08 15:43
kevin_Saizan_: Hi, this is kclancy. Here is a file demonstrating the issues that I've been having with sized types: https://paste.ofcode.org/MpBvwMzCWCHaeMJypfRN4H16/08 22:27
jonsterlingmietek: maybe you are right! It is possible that I got confused...16/08 22:51

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