Reinforce completeness of auto and totality

rlepigre / pml

New version of the PML language and (classical) proof assistant

http://pml-lang.org

MIT License

20 stars 2 forks source link

Reinforce completeness of auto and totality #28

Closed craff closed 5 years ago

craff commented 6 years ago

When instantiating a unification variable of sort value with an expression in the pool which is not a value, this does not trigger trying to prove that this a value in auto_prove. Moreover, fixing this is not enough because one should build a term which is a value to perform the instantiation.

craff commented 6 years ago

Use case in

test/insert.pml
test/vec.pml

craff commented 6 years ago

A similar issue is in

test/total.pml

craff commented 5 years ago

Seems much better if we omit issue #30. closing.