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

Mix : notation # affiché sans espace

parent ec5a7d93
......@@ -288,7 +288,7 @@ Infix "\/" := (Op Or) : formula_scope.
Infix "->" := (Op Impl) : formula_scope.
Infix "<->" := Iff : formula_scope.
Notation "# n" := (BVar n) (at level 20) : formula_scope.
Notation "# n" := (BVar n) (at level 20, format "# n") : formula_scope.
Notation " A" := (Quant All A)
(at level 200, right associativity) : formula_scope.
......
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