|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 , Verify , and At operations to eliminate principal operators of form infer , endorse , and all , 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.
|Page 761 of 800||Search logiweb.eu|