diff options
| author | Pierre-Marie Pédrot | 2018-09-28 16:59:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-28 16:59:33 +0200 |
| commit | 0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (patch) | |
| tree | 4d43a081ee4d895a7ab434f01fe31ab6b199638c /test-suite/output | |
| parent | d0122151acdbe15b88d144b730baf5b0febf3c70 (diff) | |
| parent | bfbc82eb29c9dbf868d3decbd30b0462ea398ebd (diff) | |
Merge PR #262: A cleaning step in using heuristics for inference of the return clause
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Cases.out | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index dfab400baa..cb835ab48d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -64,14 +64,9 @@ In environment texpDenote : forall t : type, texp t -> typeDenote t t : type e : texp t -t1 : type -t2 : type -t0 : type -b : tbinop t1 t2 t0 -e1 : texp t1 -e2 : texp t2 -The term "0" has type "nat" while it is expected to have type - "typeDenote t0". +n : nat +The term "n" has type "nat" while it is expected to have type + "typeDenote ?t@{t1:=Nat}". fun '{{n, m, _}} => n + m : J -> nat fun '{{n, m, p}} => n + m + p |