FINITE_CONV
pred_setLib.FINITE_CONV : conv
Proves finiteness of sets of the form {t1;...;tn}.
The conversion FINITE_CONV expects its term argument to be an
assertion of the form FINITE {t1;...;tn}. Given such a term, the
conversion returns the theorem
|- FINITE {t1;...;tn} = T
Example
> pred_setLib.FINITE_CONV ``FINITE {1;2;3}``;
val it = ⊢ FINITE {1; 2; 3} ⇔ T: thm
> pred_setLib.FINITE_CONV ``FINITE ({}:num->bool)``;
val it = ⊢ FINITE ∅ ⇔ T: thm
Failure
Fails if applied to a term not of the form FINITE {t1;...;tn}.