diff options
author | Son HO | 2023-11-22 15:06:43 +0100 |
---|---|---|
committer | GitHub | 2023-11-22 15:06:43 +0100 |
commit | bacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (patch) | |
tree | 9953d7af1fe406cdc750030a43a5e4d6245cd763 /backends/lean/Base/Primitives/Vec.lean | |
parent | 587f1ebc0178acb19029d3fc9a729c197082aba7 (diff) | |
parent | 01cfd899119174ef7c5941c99dd251711f4ee701 (diff) |
Merge pull request #45 from AeneasVerif/son_merge_types
Big cleanup
Diffstat (limited to 'backends/lean/Base/Primitives/Vec.lean')
-rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index bbed6082..e600a151 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -153,19 +153,19 @@ def Vec.coreopsindexIndexMutInst (T I : Type) @[simp] theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) : - Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i = + Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i = Vec.index_usize v i := sorry @[simp] theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) : - Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i = + Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i = Vec.index_usize v i := sorry @[simp] theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) : - Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x = + Vec.index_mut_back α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i x = Vec.update_usize v i x := sorry |