fixup diff nits

opencompl · Nov 1, 2023 · c8a2d7d · c8a2d7d
1 parent 3a97602
commit c8a2d7d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean
@@ -13,8 +13,8 @@ inductive ConcreteOrMVar (α : Type u) (φ : Nat)
 
 instance [ToString α] : ToString (ConcreteOrMVar α n) where
   toString
-  | .concrete a => s!"wconcrete({a})"
-  | .mvar i => s!"wmvar({i})"
+  | .concrete a => s!"concrete({a})"
+  | .mvar i => s!"mvar({i})"
 /-- A coercion from the concrete type `α` to the `ConcreteOrMVar` -/
 instance : Coe α (ConcreteOrMVar α φ) := ⟨.concrete⟩
 

diff --git a/SSA/Projects/MLIRSyntax/AST.lean b/SSA/Projects/MLIRSyntax/AST.lean
@@ -333,7 +333,7 @@ def AttrDict.find_nat {φ} (attrs : AttrDict φ) (name : String) : Option Nat :=
   | _ => .none
 
 def AttrDict.find_int {φ} (attrs : AttrDict φ)
-  (name : String) : Option (Int × MLIRType φ) :=
+  (name : String): Option (Int × MLIRType φ) :=
   match attrs.find name with
   | .some (AttrValue.int i ty) =>  .some (i, ty)
   | _ => .none