diff options
| -rw-r--r-- | backends/coq/Primitives.v | 2 | ||||
| -rw-r--r-- | backends/fstar/merge/Primitives.fst | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index c0056073..e6d3118f 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -67,7 +67,7 @@ Definition string := Coq.Strings.String.string. Definition char := Coq.Strings.Ascii.ascii. Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte. -Definition core_mem_replace (a : Type) (x : a) (y : a) : a * (a -> a) := (x, fun x => x) . +Definition core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) . Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }. Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }. diff --git a/backends/fstar/merge/Primitives.fst b/backends/fstar/merge/Primitives.fst index 6b8dbeb7..8011efa1 100644 --- a/backends/fstar/merge/Primitives.fst +++ b/backends/fstar/merge/Primitives.fst @@ -55,7 +55,7 @@ type string = string let is_zero (n: nat) : bool = n = 0 let decrease (n: nat{n > 0}) : nat = n - 1 -let core_mem_replace (a : Type0) (x : a) (y : a) : a & (a -> a) = (x, (fun x -> x)) +let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x) // We don't really use raw pointers for now type mut_raw_ptr (t : Type0) = { v : t } diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 321c39a8..3d70c84a 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -120,7 +120,7 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := -- MISC -- ---------- -@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × (a → a) := (x, λ x => x) +@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × a := (x, x) /-- Aeneas-translated function -- useful to reduce non-recursive definitions. Use with `simp [ aeneas ]` -/ |