From 81e991822879a942af34489b7a072f31739f28f6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jul 2023 12:37:17 +0200
Subject: Update the syntax of the progress tactic

---
 backends/lean/Base/Arith/Int.lean    | 2 +-
 backends/lean/Base/Arith/Scalar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Arith')

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 48a30a49..7a5bbe98 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
   let hs ← collectInstancesFromMainCtx lookup
   hs.toArray.mapM fun e => do
     let type ← inferType e
-    let name ← mkFreshUserName `h
+    let name ← mkFreshAnonPropUserName
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 6f4a8eba..b792ff21 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
    -- Inroduce the bounds for the isize/usize types
    let add (e : Expr) : Tactic.TacticM Unit := do
      let ty ← inferType e
-     let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false)
+     let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
    add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-- 
cgit v1.2.3