Commit ec7f8f1e authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

aggressive notations, again

parent f7734088
...@@ -169,9 +169,13 @@ Notation "∃ x , A" := (Quant Ex x A) ...@@ -169,9 +169,13 @@ Notation "∃ x , A" := (Quant Ex x A)
Definition test_form := (∃ "x", True <-> Pred "p" [Var "x";#3])%form. Definition test_form := (∃ "x", True <-> Pred "p" [Var "x";#3])%form.
Module AggressiveNotations. Module AggressiveNotations.
Local Notation "x = y" := (Pred "=" (@cons term x [y])) : formula_scope. Local Open Scope form.
(* explicit types in lists, otherwise coercions won't work well later *)
Local Notation "x = y" :=
(Pred "=" (@cons term x (@cons term y []))) : formula_scope.
Local Notation "x <> y" := (~ (x = y)) : formula_scope.
Local Notation O := (Fun "O" []). Local Notation O := (Fun "O" []).
Definition S x := (Fun "S" [x]). Local Notation S x := (Fun "S" (@cons term x [])).
Definition idvar (x:string) : variable := x. Definition idvar (x:string) : variable := x.
Local Coercion idvar : string >-> variable. Local Coercion idvar : string >-> variable.
Local Coercion Var : variable >-> term. Local Coercion Var : variable >-> term.
...@@ -180,8 +184,7 @@ Definition pred_form := ...@@ -180,8 +184,7 @@ Definition pred_form :=
(Op Impl (Not (Pred "=" [Var "x"; Fun "O" []])) (Op Impl (Not (Pred "=" [Var "x"; Fun "O" []]))
(Quant Ex "y" (Pred "=" [Var "x"; Fun "S" [Var "y"]]))). (Quant Ex "y" (Pred "=" [Var "x"; Fun "S" [Var "y"]]))).
Print pred_form. Print pred_form.
Definition pred_form_bis := Definition pred_form_bis := ∀ "x", O <> "x" -> ∃ "y", "x" = S "y".
(∀ "x", ~ "x" = O -> ∃ "y", "x" = S "y")%form.
End AggressiveNotations. End AggressiveNotations.
(** Formula printing *) (** Formula printing *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment