blob: 937bd21232d0df2dacf158dda4f0f8ffa2421a4f (
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
|
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [external]: function definitions
import Base
import External.Types
import External.FunsExternal
open Primitives
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false
namespace external
/- Trait implementation: [core::marker::{(core::marker::Copy for u32)#41}]
Source: '/rustc/library/core/src/marker.rs', lines 47:25-47:62
Name pattern: core::marker::Copy<u32> -/
def core.marker.CopyU32 : core.marker.Copy U32 := {
cloneCloneInst := core.clone.CloneU32
}
/- [external::use_get]:
Source: 'tests/src/external.rs', lines 9:0-9:37 -/
def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
core.cell.Cell.get U32 core.marker.CopyU32 rc st
/- [external::incr]:
Source: 'tests/src/external.rs', lines 13:0-13:31 -/
def incr
(rc : core.cell.Cell U32) (st : State) :
Result (State × (core.cell.Cell U32))
:=
do
let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
let i1 ← i + 1#u32
let (_, rc1) ← get_mut_back i1 st1
Result.ok (st1, rc1)
end external
|
