File: RegressionTests.ref

package info (click to toggle)
coq-record-update 0.3.6-2
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 208 kB
  • sloc: makefile: 38; sed: 6
file content (11 lines) | stat: -rw-r--r-- 448 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
 
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (fun (r : X) (a : nat) => r <| getA := a |>)
More precisely: 
- ?Setter: Cannot infer the implicit parameter Setter of set whose type is
  "Setter getA" (no type class instance found) in environment:
  r : X
  a : nat
test =
fun (s : ThreadState) (newRegs : Registers) => s <| Regs := newRegs |>
     : ThreadState -> Registers -> ThreadState