[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Help with TCCs

Dear Nikhil Varma,

You need to cite suitable lemmas from the prelude.  E.g., for
  (skosimp) (lemma "nnreal_div_posreal_is_nnreal") (inst?)
will do the job.

Note that if you replace your types NZTR and ZTR by the predefined
types posreal and nonneg_real, respectively, then the judgments in the
prelude allow the typechecker to discharge the tccs internally and
they will not be generated.  If you want to keep your own types NZTR
and ZTR, then just define suitable judgments for them and discharge
the tccs once and for all.

If you want to see how the judgment lemmas are proved, just do
edit-proof (or step-proof) on the ones in the prelude.

Good luck,
John Rushby