0
Unter Befestigung ist eine halbe Arbeits einfache rekursive Notation:Coq: eine rekursive Notation
Universe ARG. Definition ARG := [email protected]{ARG}.
Parameter X: ARG.
Notation A := (fun x:ARG->ARG => fun y:x X => y).
Parameter P: ARG -> ARG.
Parameter s: P X.
Notation "[ x .. z u ]" := (x P .. (z P u) ..) (at level 5, z, u at next level).
Check (A P (A P (A P s))). (* [A A A s]: P X *)
Print Grammar constr.
(*| "5" RIGHTA
[ "["; NEXT; LIST1 NEXT; NEXT; "]"
| "["; NEXT; NEXT; "]" ]*)
Check [A A A s]. (* Syntax error: [constr:operconstr] or [constr:operconstr] expected (in [constr:operconstr]). *)
Wie Sie sehen, erkennt Coq A P (A P (A P s)) als [A A A s]: P X kann aber [A A A s] nicht analysieren. Wo ist das Problem, was ist das Problem?
EDIT: Coq scheint hier einige "Parsing Aids" zu benötigen. Zum Beispiel sind die folgenden Werke:
Notation "(x .. z [ u ])" := (x P .. (z P u) ..) (at level 5, z at next level).
Check (A A A [s]): P X.
Wie ich loswerden der inneren Notation erhalten möchte, bleibt die Frage offen