Rename # to #'

JetBrains · Jun 24, 2024 · 793ac39 · 793ac39
1 parent 80e548a
commit 793ac39
Show file tree

Hide file tree

Showing 7 changed files with 20 additions and 20 deletions.
diff --git a/meta/src/main/java/org/arend/lib/StdExtension.java b/meta/src/main/java/org/arend/lib/StdExtension.java
@@ -270,7 +270,7 @@ public void declareDefinitions(@NotNull DefinitionContributor contributor) {
     MetaDefinition apply = new ApplyMeta(this);
     ModulePath function = ModulePath.fromString("Function.Meta");
     contributor.declare(function, new LongName("$"), "`f $ a` returns `f a`", new Precedence(Precedence.Associativity.RIGHT_ASSOC, (byte) 0, true), apply);
-    contributor.declare(function, new LongName("#"), "`f # a` returns `f a`", new Precedence(Precedence.Associativity.LEFT_ASSOC, (byte) 0, true), apply);
+    contributor.declare(function, new LongName("#'"), "`f #' a` returns `f a`", new Precedence(Precedence.Associativity.LEFT_ASSOC, (byte) 0, true), apply);
     contributor.declare(function, new LongName("repeat"),
       """
         `repeat {n} f x` returns `f^n(x)

diff --git a/src/Algebra/Domain/Euclidean.ard b/src/Algebra/Domain/Euclidean.ard
@@ -427,10 +427,10 @@
 
 \lemma nat_gcd_sum (a b d : Nat) : gcd (a + b * d) b = gcd a b
   => \let a' => a + b * d
-     \in equation                     #
-         gcd a' b                     # {nat_gcd-isUnique (gcd-isGCD a' b) (gcd_int_nat (gcd-isGCD (pos a') (pos b)))}
-         iabs (gcd (pos a') (pos b))  # {int_gcd-isUnique (gcd-isGCD (pos a') (pos b)) (GCDDomain.gcd_sum (pos d) (gcd-isGCD (pos a) (pos b)))}
-         iabs (gcd (pos a) (pos b))   # {inv (nat_gcd-isUnique (gcd-isGCD a b) (gcd_int_nat (gcd-isGCD (pos a) (pos b))))}
+     \in equation                     #'
+         gcd a' b                     #' {nat_gcd-isUnique (gcd-isGCD a' b) (gcd_int_nat (gcd-isGCD (pos a') (pos b)))}
+         iabs (gcd (pos a') (pos b))  #' {int_gcd-isUnique (gcd-isGCD (pos a') (pos b)) (GCDDomain.gcd_sum (pos d) (gcd-isGCD (pos a) (pos b)))}
+         iabs (gcd (pos a) (pos b))   #' {inv (nat_gcd-isUnique (gcd-isGCD a b) (gcd_int_nat (gcd-isGCD (pos a) (pos b))))}
          gcd a b
 
 \func nat_gcd_*_div {a b c : Nat} (a|bc : LDiv a (b * c)) (a_b : gcd a b = 1) : LDiv a c

diff --git a/src/Algebra/Ring/Poly.ard b/src/Algebra/Ring/Poly.ard
@@ -28,7 +28,7 @@
 \import Equiv.Fiber
 \import Equiv.Univalence
 \import Function \hiding (id,o)
-\import Function.Meta \hiding (#)
+\import Function.Meta
 \import HLevel
 \import Logic
 \import Logic.Meta

diff --git a/src/Data/List.ard b/src/Data/List.ard
@@ -4,7 +4,7 @@
 \import Data.Bool
 \import Data.Or
 \import Function
-\import Function.Meta \hiding (#)
+\import Function.Meta
 \import Logic
 \import Logic.Meta
 \import Meta

diff --git a/src/Logic/Rewriting/TRS/Union/Confluence.ard b/src/Logic/Rewriting/TRS/Union/Confluence.ard
@@ -6,7 +6,7 @@
 \import Data.Shifts
 \import Data.SubList
 \import Data.Or
-\import Function.Meta \hiding (#)
+\import Function.Meta
 \import Logic
 \import Logic.Meta
 \import Paths

diff --git a/src/Topology/Compact.ard b/src/Topology/Compact.ard
@@ -3,7 +3,7 @@
 \import Data.Or
 \import Equiv
 \import Function
-\import Function.Meta \hiding (#)
+\import Function.Meta
 \import Logic
 \import Logic.Meta
 \import Meta

diff --git a/test/Algebra/EquationalReasoningTest.ard b/test/Algebra/EquationalReasoningTest.ard
@@ -4,23 +4,23 @@
 \import Paths
 
 \lemma test1 (f : Nat -> Nat) (x y z : Nat) (p : f x = y) (q : f y = z) (s : z = f x) : f z = z
-  => equation # {pmap f s}
-     f (f x)  # {pmap f p}
-     f y      # {q}
+  => equation #' {pmap f s}
+     f (f x)  #' {pmap f p}
+     f y      #' {q}
 
 \lemma test2 (f : Nat -> Nat) (x y z : Nat) (p : f x = y) (q : f y = z) (s : z = f x) : f z = z
-  => \let t => equation #
-      f z      # {pmap f s}
-      f (f x)  # {pmap f p}
-      f y      # {q}
+  => \let t => equation #'
+      f z      #' {pmap f s}
+      f (f x)  #' {pmap f p}
+      f y      #' {q}
       z
     \in t
 
 \lemma test3 (f : Nat -> Nat) (x y z : Nat) (p : f x = y) (q : f y = z) (s : z = f x) : f z = z
-  => equation #
-     f z      # {pmap f s}
-     f (f x)  # {pmap f p}
-     f y      # {q}
+  => equation #'
+     f z      #' {pmap f s}
+     f (f x)  #' {pmap f p}
+     f y      #' {q}
      z
 
 \lemma test4 : 0 = 0