2
$\begingroup$

How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq?

A similar notation (but without quantifiers) appears here

Notation "x ≤ y  ≤ ..  ≤ z ≤ t" :=
    ((fun b A a => a <= b /\ A b) y 
 .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) 
 .. x)
  (at level 70, y at next level, z at next level, t at next level).

But I was unsuccessful in putting forall quantifiers to it.

$\endgroup$
1

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.