Library Coq.ssrmatching.ssrmatching
Module SsrMatchingSyntax.
Reserved Notation "( a 'in' b )" (
at level 0).
Reserved Notation "( a 'as' b )" (
at level 0).
Reserved Notation "( a 'in' b 'in' c )" (
at level 0).
Reserved Notation "( a 'as' b 'in' c )" (
at level 0).
Delimit Scope ssrpatternscope with pattern.
Notation "( X 'in' t )" := (
_ :
fun X =>
t) :
ssrpatternscope.
Notation RHS :=
(X in _ = X)%
pattern.
Notation LHS :=
(X in X = _)%
pattern.
End SsrMatchingSyntax.
Export SsrMatchingSyntax.
Tactic Notation "ssrpattern"
ssrpatternarg(
p) :=
ssrpattern p .