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/Alloc.lean | |
parent | 587f1ebc0178acb19029d3fc9a729c197082aba7 (diff) | |
parent | 01cfd899119174ef7c5941c99dd251711f4ee701 (diff) |
Merge pull request #45 from AeneasVerif/son_merge_types
Big cleanup
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives/Alloc.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean index 34590499..6c89c6bb 100644 --- a/backends/lean/Base/Primitives/Alloc.lean +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -16,16 +16,16 @@ def deref_mut (T : Type) (x : T) : Result T := ret x def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x /-- Trait instance -/ -def coreOpsDerefInst (Self : Type) : +def coreopsDerefInst (Self : Type) : core.ops.deref.Deref Self := { Target := Self deref := deref Self } /-- Trait instance -/ -def coreOpsDerefMutInst (Self : Type) : +def coreopsDerefMutInst (Self : Type) : core.ops.deref.DerefMut Self := { - derefInst := coreOpsDerefInst Self + derefInst := coreopsDerefInst Self deref_mut := deref_mut Self deref_mut_back := deref_mut_back Self } |