in_1 is being used before being axiomated

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.

1 stars 0 forks source link

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

(forall ((this Atom)) (=> (in_1 this FSO) (or (in_1 this File) (in_1 this Dir))))

jonnybest commented 12 years ago

"in" does not have an axiom. it's uninterpreted