search

rlepigre / pml

New version of the PML language and (classical) proof assistant
http://pml-lang.org
MIT License
20 stars 2 forks source link

Error managment in Raw module (mantis #46) #11

Open craff opened 6 years ago

craff commented 6 years ago

various forbidden case due to sorting that have no error generated

craff commented 6 years ago

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

rlepigre commented 6 years ago

T'as un exemple minimal ?

craff commented 6 years ago

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 commented 6 years ago

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