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. 
16:56 
barrucadu 
Ok, thanks 