diff options
| author | Son Ho | 2024-03-11 09:43:21 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-11 09:43:21 +0100 |
| commit | bf0b35b9b1fa90d50587e906432077b63a9ad34d (patch) | |
| tree | 76507daab5827cdca8f75aea975deb5d0b9aed2f /tests/coq/demo | |
| parent | 5af8412b48aef44448d3ce674612aa18feb961b3 (diff) | |
Update the generated files
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/demo/Demo.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index 1abe7c5c..22a0a131 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -145,16 +145,16 @@ Record Counter_t (Self : Type) := mkCounter_t { Arguments mkCounter_t { _ }. Arguments Counter_t_incr { _ }. -(** [demo::{usize}::incr]: +(** [demo::{(demo::Counter for usize)}::incr]: Source: 'src/demo.rs', lines 88:4-88:31 *) -Definition usize_incr (self : usize) : result (usize * usize) := +Definition counterUsize_incr (self : usize) : result (usize * usize) := self1 <- usize_add self 1%usize; Return (self, self1) . -(** Trait implementation: [demo::{usize}] +(** Trait implementation: [demo::{(demo::Counter for usize)}] Source: 'src/demo.rs', lines 87:0-87:22 *) -Definition demo_CounterUsizeInst : Counter_t usize := {| - Counter_t_incr := usize_incr; +Definition CounterUsize : Counter_t usize := {| + Counter_t_incr := counterUsize_incr; |}. (** [demo::use_counter]: |