Re: [isabelle] Error: Pending sort hypothesis

Hi Peter,

Peter Lammich schrieb:

> lemma
>   fixes A :: "'a set"
>   assumes "finite A"
>   obtains f::"'a => nat" and n::"nat" where
>     "f`A = {i. i<n}"
>     "inj_on f A"

> *** Pending sort hypotheses: {finite,semiring_char_0}
> *** At command "done".

Pending sort hypothesis are sort constraints which a theorem's proof
relies one, but whose type variables do not occur in the theorem
proposition; the have to be given explicitly in the assumptions, e.g.

	assumes "SORT_CONSTRAINT('a::{finite,semiring_char_0})"

or whatever type variable 'x they refer too.

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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