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

use closure in the pool Description (mantis #40) #18

Closed craff closed 6 years ago

craff commented 6 years ago

the binder in all pool node (equiv.ml module) should be replaced by closure.

This will allow to know that

a = b => (fun x y -> y x) a = (fun x y -> y x) b

without using an oracle

craff commented 6 years ago

Done.