Re: [isabelle] Isar parser for constant names

On Mon, 19 May 2014, Moa Johansson wrote:

I though I’d make use of the function Parse.const. However, although this function parses the constant name to a string, it appears it is not the same one as passing the function names explicitly as a string, which I would expect.

Parse.const is the right thing, but only half of it, namely the outer syntax parser. You also need an inners syntax "read" function.

Peeking at the implementation of the 'notation' command suggests the following:

  Proof_Context.read_const ctxt false dummyT


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.