Re: [isabelle] I need a meta-or



On Wed, 31 Jul 2013, Gottfried Barrow wrote:

It's a syntax priority problem.

Trueprop priority is 5, so dealing with the syntax of functions of type "prop => prop" and "prop => prop => prop" is tricky:

  Trueprop :: "bool => prop"   ("(_)" 5)

If you want to play with syntax, you can always use 'notation' and 'no_notation' to specify things in any way you like, but don't ask me about suitable priorities -- this is a black art and better not changed fundamentally.

Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic to reason about other logics. It is just a logical framework, for higher-order natural deduction based on !! and ==>.

If you really want to reason about some other logic, better do it in Isabelle/HOL, and define you syntax as datatype, semantics as function, inference system as inductive predicate in the usual way. AFP has examples for that.


	Makarius




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