diff options
| author | Son HO | 2024-06-13 22:56:37 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-13 22:56:37 +0200 |
| commit | 8e3fe11c1b31eafe14806bb513b51530c6eb99ec (patch) | |
| tree | c101e6bffaf474da394229fa4bda3147409577a0 /backends/lean/Base/Primitives/ArraySlice.lean | |
| parent | 234fa36da87b672397f96098bcf832d869f2cfbb (diff) | |
| parent | d5cf75a0f8209298ad85f46249f14d5c3a24faf6 (diff) | |
Merge pull request #243 from AeneasVerif/son/update-lean
Update Lean to v4.9.0-rc1
Diffstat (limited to 'backends/lean/Base/Primitives/ArraySlice.lean')
| -rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 17ee626f..be460987 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -325,8 +325,7 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac) simp [*] -attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing -set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse) +set_option pp.fieldNotation.generalized true def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) := -- TODO: not completely sure here |