Stream: Hydras & Co. universe

Topic: New notations

view this post on Zulip 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))) ?

view this post on Zulip 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

Last updated: Jun 11 2023 at 00:30 UTC