Skip to content

Commit

Permalink
chroe: fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@leodemoura
leodemoura committed Jan 3, 2024
1 parent cb4d044 commit 06f577f
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 9 deletions.
2 changes: 1 addition & 1 deletion tests/lean/2040.lean.expected.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,4 +9,4 @@
has type
a = @OfNat.ofNat Nat 2 (instOfNatNat 2) ^ n : Prop
but is expected to have type
a = @OfNat.ofNat Int 2 ofNatInst ^ n : Prop
a = @OfNat.ofNat Int 2 instOfNat ^ n : Prop
16 changes: 8 additions & 8 deletions tests/lean/2220.lean.expected.out
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@ofNatInst 3))
@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
(@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@ofNatInst 1))
(@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@ofNatInst 3))
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
(@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
(@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@ofNatInst 1))
(@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@ofNatInst 3))
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1))
(@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
(@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@ofNatInst 3))
@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3))
(@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
2220.lean:25:19-25:24: error: failed to synthesize instance
HPow Nat Nat Int
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@ofNatInst 1))
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@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 instance
HPow Nat Nat Int
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@ofNatInst 1))
@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@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

0 comments on commit 06f577f

Please sign in to comment.