Logiweb(TM)

14.290 Cannot convert r to type t

Prev Up Next Page 761 of 800 Search internet


Origin: check or Peano. Landing-place: diagnose.

Cannot convert r to type ``t''

The unification tactic tries to modify argumentations to fit a conclusion. It does so by adding Ponens x Ponens, Verify x Verify, and At x at y operations to eliminate principal operators of form infer x infer y, endorse x endorse y, and all All x : y, respectively. The unification tactic proceeds this way until it reaches a conclusion of the desired type t (which may be infer, endorse, or all) or until it can remove no more principal operators. In the latter case the unification tactic emits a 'Cannot convert r to type t' message.

The term x is given out of context and after macro and tactic expansion, so start out by locating the error.

Prev Up Next Page 761 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05