Что означают символы/и || представляют в Coq?

Question

Что означают символы / и || в coq? Я проверил справочное руководство и искал в Интернете, но не смог его найти.

Answer 1

Эти символы (как и большинство операторов) могут быть переопределены. Это зависит от контекста.

Вы получите наиболее точный ответ, запросив Coq.

Использование, например. Locate "||"., чтобы отобразить все текущие обозначения, содержащие токен ||.

Если вы не уверены, какие обозначения используются в определенном выражении, попросите Coq распечатать его с отключенной печатью.

Unset Printing Notations. 
Check (fun a b => a || b). 
Set Printing Notations.