Error managment in Raw module (mantis #46)

[craff]

various forbidden case due to sorting that have no error generated

[craff]

Les deduces qui échouent (sans doute show aussi ?) lève une exception non rattrapée

[rlepigre]

T'as un exemple minimal ?

[craff]

On 17-11-21 17:02:14, Rodolphe Lepigre wrote: T'as un exemple minimal ?

Je finis de merger master dans totality (je fais dans ce sens pour garder master encore un peu) et je t'envoie ça. A+ Christophe

…

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.*

[craff]

On 17-11-21 17:02:14, Rodolphe Lepigre wrote: T'as un exemple minimal ? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.*

Salut, Tu prends nat_proofs.pml, premier deduce et tu changes le dernier n en p, et tu obtiens: [ERR] Type error: {} : ((add) (n)) (p)≡((add) (((add) (Zero)) (n))) (n) [ERR] Subtype error: {} ∈ {} ⊂ ((add) (n)) (p)≡((add) (((add) (Zero)) (n))) (n) [ERR] Failed to prove an equational relation. [ERR] ((add) (n)) (p) = ((add) (((add) (Zero)) (n))) (n) On n'a pas la position. A+ Christophe