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
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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