diff options
| author | Son Ho | 2023-07-26 12:37:17 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-26 12:37:17 +0200 |
| commit | 81e991822879a942af34489b7a072f31739f28f6 (patch) | |
| tree | 05f9891ff640c75d7dbfb8714e8dc9d99c092a62 /backends/lean/Base/Arith | |
| parent | 032db82439d9b379b5435d8349c1ecf55eeb2875 (diff) | |
Update the syntax of the progress tactic
Diffstat (limited to 'backends/lean/Base/Arith')
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 2 |
2 files changed, 2 insertions, 2 deletions
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 []]) |