--- Day changed Tue Aug 22 2017
zephyz_Hi, I'm reading through Total Parser Combinators by Nils Anders Danielsson and one of the data constructors is this `cast:s ∈ p → s ∈ cast eq p`22/08 20:51
zephyz_does anyone know what `eq` is?22/08 20:51
zephyz_it's not mentioned anywhere in the paper and I cannot find anything on the web 22/08 20:52
zephyz_and it does not seem to be an instance of Equiv since none of relf, sym or `trans` are implemented22/08 20:54
adamsezephyz_: the eq there is probably an implicit argument to the constructor cast which has been hidden in the paper version22/08 21:15
adamseI think you are looking at what corresponds to http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators/TotalParserCombinators.Semantics.html#2535 in the agda code22/08 21:16
zephyz_ah I see22/08 21:17
zephyz_I'm looking at recognisers at the moment so there is no bag equality but22/08 21:19
zephyz_it made me realise that the constructor for cast is actually `cast : ∀{n1 n2}→n1 ≡ n2 →Pn1 →Pn2`22/08 21:20
zephyz_so I guess the first argument is a proof that n1 = n222/08 21:20
zephyz_does that mean that eq is just Relf?22/08 21:20
adamsezephyz_: I think so, or something that evaluates to refl22/08 21:22
zephyz_I see, thank you22/08 21:22
adamsethere are two different constructors cast involved here, something not too unusual in Agda is to use the same constructor names for your semantics as for your terms22/08 21:27
zephyz_Yes I see22/08 21:29

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