summaryrefslogtreecommitdiff
path: root/tests/coq/misc/External_Funs.v
blob: d0de80d996fb90e43a9f0d9acf5a4a078bb71142 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: function definitions *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
Require Import External_Types.
Include External_Types.
Require Import External_FunsExternal.
Include External_FunsExternal.
Module External_Funs.

(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#61}]
    Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/marker.rs', lines 47:29-47:65
    Name pattern: core::marker::Copy<u32> *)
Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {|
  core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32;
|}.

(** [external::use_get]:
    Source: 'tests/src/external.rs', lines 5:0-5:37 *)
Definition use_get
  (rc : core_cell_Cell_t u32) (st : state) : result (state * u32) :=
  core_cell_Cell_get u32 core_marker_CopyU32 rc st
.

(** [external::incr]:
    Source: 'tests/src/external.rs', lines 9:0-9:31 *)
Definition incr
  (rc : core_cell_Cell_t u32) (st : state) :
  result (state * (core_cell_Cell_t u32))
  :=
  p <- core_cell_Cell_get_mut u32 rc st;
  let (st1, p1) := p in
  let (i, get_mut_back) := p1 in
  i1 <- u32_add i 1%u32;
  p2 <- get_mut_back i1 st1;
  let (_, rc1) := p2 in
  Ok (st1, rc1)
.

End External_Funs.