Re: [isabelle] Ambiguous input



> in Test.thy file i have made an abbreviation subset_b
> but in output it gave me in output an Ambiguous input but i don’t know why ? and where is the problem ?

The problem already occurs earlier, in your function definition:

> Variable "subst" occurs on right hand side only:
> ⋀x a a1 a2 subst. substb x a (Less a1 a2) = Less (subst x a a1) (subst x a a2)

It seems to me that you defined "subst" somewhere else, but didn't
include it in the theory file you attached.

After fixing this, the ambiguity error goes away. You might still want
to define some other syntax, or at least give a fixity annotation,
because "[a/b]" could also denote the list containing the value "a/b".







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