aarushgupta's picture
Deploy FATHOM-DM Space bundle
2803d7e verified
type readable : t {
predicates {
free_read(readable);
read_requires(readable, o);
prepared(readable);
read_keeps_use(readable);
read_consumes_use(readable);
}
rules {
read/free :: $at(P, r) & $at(readable, r) & $free_read(readable) -> at(P, r);
read/prepared :: $at(P, r) & $at(readable, r) & $prepared(readable) -> at(P, r);
use/readable/keep :: $at(P, r) & $at(readable, r) & $in(o, I) & $read_requires(readable, o) & $read_keeps_use(readable) -> prepared(readable);
use/readable/consume :: $at(P, r) & $at(readable, r) & in(o, I) & $read_requires(readable, o) & $read_consumes_use(readable) -> prepared(readable);
}
reverse_rules {
read/free :: read/free;
read/prepared :: read/prepared;
use/readable/keep :: use/readable/keep;
use/readable/consume :: use/readable/consume;
}
inform7 {
type {
kind :: "readable-like";
definition :: "readable-like is a kind of thing. readable-like is fixed in place.";
}
predicates {
free_read(readable) :: "";
read_requires(readable, o) :: "";
prepared(readable) :: "";
read_keeps_use(readable) :: "";
read_consumes_use(readable) :: "";
}
commands {
read/free :: "read {readable}" :: "examining the {readable}";
read/prepared :: "read {readable}" :: "examining the {readable}";
use/readable/keep :: "use {o} on {readable}" :: "unlocking the {readable} with the {o}";
use/readable/consume :: "use {o} on {readable}" :: "unlocking the {readable} with the {o}";
}
code :: """
Understand "read [something]" as examining.
Understand "use [something] on [something]" as unlocking it with.
""";
}
}