Commit 5325f9f0 authored by Ralf Jung's avatar Ralf Jung

put notation into stdpp_scope

parent 05ffdc9b
......@@ -143,7 +143,7 @@ Notation "'[tele_arg' ]" := (TargO)
Notation "'λ..' x .. y , e" :=
(tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
(at level 200, x binder, y binder, right associativity,
format "'[ ' 'λ..' x .. y ']' , e").
format "'[ ' 'λ..' x .. y ']' , e") : stdpp_scope.
(** Telescopic quantifiers *)
Definition tforall {TT : tele} (Ψ : TT Prop) : Prop :=
......
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