upd: reduction_sys for generating notations for reductions and the multi-step closure

Author: zayn7lie

Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean

@@ -39,6 +39,7 @@ namespace Lambda
 open Term
 
 /-- One-step β-reduction (compatible closure). -/
+@[reduction_sys "β"]
 public inductive Beta : Term → Term → Prop
   | abs  {t t'}        : Beta t t' → Beta (λ.t) (λ.t')
   | appL {t t' u}      : Beta t t' → Beta (t·u) (t'·u)

Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean

@@ -41,6 +41,7 @@ namespace Lambda
 open Term
 
 /-- Parallel β-reduction (syntax-directed). -/
+@[reduction_sys "∥"]
 public inductive Par : Term → Term → Prop
   | var (n) : Par (𝕧 n) (𝕧 n)
   | abs {t t'} : Par t t' → Par (λ.t) (λ.t')