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) (only parsing) : ssrpatternscope.

Notation RHS := (X in _ = X)%pattern.
Notation LHS := (X in X = _)%pattern.

End SsrMatchingSyntax.

Export SsrMatchingSyntax.

Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p .