Merge branch 'leanprover:main' into main

Author: WegmannDavid

Cslib/Foundations/Syntax/Congruence.lean

@@ -15,6 +15,6 @@ namespace Cslib
 
 /-- An equivalence relation preserved by all contexts. -/
 class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
-  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·[·]) r
+  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
 
 end Cslib

Cslib/Foundations/Syntax/Context.lean

@@ -19,6 +19,6 @@ class HasContext (Term : Sort*) where
   /-- Replaces the hole in the context with a term. -/
   fill (c : Context) (t : Term) : Term
 
-@[inherit_doc] notation:max c "[" t "]" => HasContext.fill c t
+@[inherit_doc] notation:max c "<[" t "]" => HasContext.fill c t
 
 end Cslib

Cslib/Languages/CCS/Basic.lean

@@ -123,14 +123,14 @@ instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Conte
 
 /-- Definition of context filling. -/
 @[scoped grind =]
-theorem isContext_def (c : Context Name Constant) (p : Process Name Constant) :
-  c[p] = c.fill p := rfl
+theorem hasContext_def (c : Context Name Constant) (p : Process Name Constant) :
+  c<[p] = c.fill p := rfl
 
 /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context`
 is a complete formalisation of syntactic contexts for CCS. -/
 theorem Context.complete (p : Process Name Constant) :
-    ∃ c : Context Name Constant, p = c[Process.nil] ∨
-    ∃ k : Constant, p = c[Process.const k] := by
+    ∃ c : Context Name Constant, p = c<[Process.nil] ∨
+    ∃ k : Constant, p = c<[Process.const k] := by
   induction p
   case nil =>
     exists hole