diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/demo/Demo.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index 1abe7c5c..ec7ca29d 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -145,23 +145,23 @@ 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]: Source: 'src/demo.rs', lines 95:0-95:59 *) Definition use_counter - (T : Type) (counterTInst : Counter_t T) (cnt : T) : result (usize * T) := - counterTInst.(Counter_t_incr) cnt + (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) := + counterInst.(Counter_t_incr) cnt . End Demo. |