Pierre Castéran (Feb 26 2023 at 17:25): Pierre Castéran (Feb 26 2023 at 17:25):I'm thinking about the design of simple notations for FOL-formulas.
In Ackermann+Gödel, a formula like (andH _ A B) can be reduced to (notH _ (orH _ (notH _ A) (notH _ B))), or worse,
to (notH _ (impH _ (notH _ (notH _ A)) (notH _ B))) (same stuff for all derived connectors and quantifiers).
I'm not sure if a given notation can be bound to several different terms.
A solution could be to bind A /\ B to (andH _ A B), and a specific notation to the most expanded form (in goals or results of Computecommands), like (A /\x B) for (notH _ (impH _ (notH _ (notH _ A)) (notH _ B))) ?
Karl Palmskog (Feb 26 2023 at 17:48):maybe add some small marker to differentiate the deep embedding from Coq operators? like _/\. I wonder if we can take inspiration from https://github.com/dominik-kirst/coq-library-undecidability/tree/fol-library/theories/FOL
Last updated: Jun 11 2023 at 00:30 UTC