--- Day changed Fri Feb 09 2018
apostolispgiarrusso : Yes, I would like agda to do that. I want to use instance arguments to hold proof that a resource / variable has been used or not.09/02 00:01
apostolisI do not want the programer to prove this for any variable he uses in a function. 09/02 00:02
apostolisTo have inductive / coinductive "variables" , one needs to have a proof that its parts has not been used / or freed.09/02 00:05
skihm, can one define syntax where the type of a lexically earlier subexpression depends on the value of a later one ?09/02 18:36
dolioski: Yes.09/02 20:14
skihow does one specify that ?09/02 20:16
dolioFirst you'd define something where the dependency is in the normal lexical order, then define syntax for it that flips it around.09/02 20:17
skii've done that when i wanted the index of a data type before a parameter. but i don't know how to do that, when there's a dependency in the type09/02 20:20
skiin Agda1, iirc, you could write something like `$1',`$2',... in the name, to indicate where the operands would go, possibly out of order09/02 20:21
dolioDo you mean you've done it with a function, or with a syntax declaration?09/02 20:22
skiiirc, one could do something like09/02 20:23
dolioLike, you should be able to do `asType : (A : Set) -> A -> A` and then `syntax x :: A = asType A x`.09/02 20:24
ski  foo'$2'bar'$1'baz :: (a :: A) -> P a -> Q a  -- in Agda1, i.e.09/02 20:24
skiok, `syntax' was the relevant keyword09/02 20:24

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