Làm cách nào để vô hiệu hóa ký hiệu tùy chỉnh của tôi trong Coq?

Question

tôi đã xác định một ký hiệu để mô phỏng lập trình phong cách bắt buộc bởi

Notation "a >> b" := (b a) (at level 50). 

Tuy nhiên sau đó, tất cả các biểu hiện chức năng ứng dụng được biểu diễn như phong cách '>>'. Ví dụ, trong chế độ bằng chứng về Coq mục cấp đầu, tôi có thể thấy

bs' : nat >> list 

trong khi thực sự cần

bs' : list nat 

Tại sao Coq tích cực viết lại tất cả các ứng dụng chức năng biểu hiện theo kiểu vào tôi tùy chỉnh '>>' đại diện? Làm cách nào để khôi phục mọi thứ trở lại bình thường, tôi muốn xem 'a >> b' được hiểu là 'b a' và 'list nat' sẽ không được biểu diễn dưới dạng 'nat >> list'?

Cảm ơn bạn!

Answer 1

Theo mặc định, Coq giả định rằng nếu bạn định nghĩa một ký hiệu, bạn muốn nó cho khá-in . Nếu bạn muốn ký hiệu không bao giờ xuất hiện trong quá trình in đẹp, hãy khai báo nó là "chỉ phân tích cú pháp".

Notation "a >> b" := (b a) (at level 50, only parsing). 

Nếu bạn muốn a >> b hiển thị đôi khi, bạn có thể giới hạn phạm vi và kết hợp loại này với phạm vi này; thì ký pháp sẽ chỉ được áp dụng khi loại kết quả là loại đó.

Không có cách nào để nói với Coq “chỉ sử dụng ký hiệu khi tôi sử dụng nó trong mã nguồn”, vì cụm từ được viết bằng ký hiệu giống hệt với cụm từ được viết theo bất kỳ cách nào khác: ký hiệu được sử dụng ban đầu là không phải là một phần của thuật ngữ.

Answer 2

Bạn có thể sử dụng định nghĩa thay thế. Bằng cách này, chỉ những thứ bạn gắn thẻ là "followingBy" sẽ được hợp nhất theo cách này. Nếu không có cách nào cho máy tính để biết khi nào cần sử dụng một không gian so với ">>" ...

Definition followedBy {A B : Type} (a : A) (b : A -> B) := b a. 

Notation "a >> b" := (followedBy a b) (at level 50).