de5e039c83
Summary: - Take `synthPendingDepth` into account when caching TC results - Add `maxSynthPendingDepth` option with default := 2. - Add support for tracking `synthPending` failures when using `set_option diagnostics true` closes #2522 closes #3313 closes #3927 Identical to #4114 but with `maxSynthPendingDepth := 1` closes #4114 cc @semorrison
18 lines
1.3 KiB
Text
18 lines
1.3 KiB
Text
@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
|
|
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
|
|
(@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
|
|
(@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
|
|
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
|
|
(@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
|
|
(@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
|
|
@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
|
|
2220.lean:25:19-25:24: error: failed to synthesize
|
|
HPow Nat Nat Int
|
|
use `set_option diagnostics true` to get diagnostic information
|
|
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
|
|
(@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
|
|
2220.lean:26:12-26:17: error: failed to synthesize
|
|
HPow Nat Nat Int
|
|
use `set_option diagnostics true` to get diagnostic information
|
|
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
|
|
(@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
|