# IRC log for #isabelle, 2016-01-11

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
12:53 ilbot3 joined #isabelle
12:53 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
14:38 barrucadu I have a typedef for finite maps, `typedef ('k, 'v) fmap = "{M :: ('k â 'v). finite (dom M)}"`, and I'm having an issue with lifting a definition due to a missing relator ("No relator for the type "FMap.fmap" found.").
14:38 barrucadu How do I define a relator?
14:39 barrucadu I have proven this to be a BNF, so I do have some sort of relation function, but that doesn't seem to be enough
14:45 larsrh barrucadu: If you figure it out, tell me :-)
14:58 ThreeOfEight barrucadu: fyi, there are already two implementations of finite maps in Isabelle
14:59 ThreeOfEight also, anything that has to do with BNFs is probably a good question for the mailing list
14:59 ThreeOfEight I dare say that the BNF experts are not really in this channel
15:00 barrucadu ThreeOfEight: There's AList, which I had difficulty using because of list ordering issues, what's the other?
15:08 larsrh barrucadu: He's referring to FinFun and FinMap
15:09 larsrh FinFun is not really a finite map implementation (it's more general than what you have posted)
15:09 larsrh I can't say much about FinMap
15:12 ThreeOfEight I'm trying to look up Fin_Map, but Isabelle/jEdit is being difficult again
15:17 barrucadu Hmm, neither FinFun nor Fin_Map define BNFs, so I'd need to do that
15:18 ThreeOfEight ah, Fin_Map essentially requires that everything outside the domain maps to undefined
15:37 ThreeOfEight barrucadu: what exactly is failing?
15:37 ThreeOfEight i.e. what definition fails?
15:52 barrucadu ThreeOfEight: There's a bit of clutter there, but it's the definition at the end: https://gist.github.com/barrucadu/a4a32ecb19eb63047bc6
15:55 ThreeOfEight barrucadu: I think I probably need your other files, too
15:55 ThreeOfEight especially the definition of Fmap
16:06 barrucadu ThreeOfEight: I've updated the gist
16:10 ThreeOfEight you should really write "~~/src/HOL/Library/FSet" in the imports
16:55 ThreeOfEight barrucadu: I'll get back to you on that.