A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17
stars
2
forks
source link
[Substitution] Substitution with definition #153
Closed
olaure01 closed 3 years ago
It seems definitions are not taken into account as targets of substitutions thus generating some error. For example, try to substituted
X ::= Ain: http://localhost:3000/?s=I&n=I%2CX+-o+X&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslNJFpPncDNqmC0%2BGDWpnpdCAR6c9SAGSHm%2BINkWc8IfafrwTqc8V8eb49BHr9D2VBF1BL%2BKEgEsR74aISfi5GhXrx%2B6qjsOHwacUkBQTjiM4AQeomyvO34ht71v6N5xkJto7aPfkm9O2q8y3XNV1KnH%2B2zU%2F4OsqRnql2N6De81VfH8t8tBz445KVUFh6S%2BJ1uTkaBJ0sVlNv%2F%2BCCbQv