08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
47 lines
3 KiB
Text
47 lines
3 KiB
Text
@instCoeTOfCoeHTCT
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Nat
|
|
(@Subtype.mk Nat (fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
|
|
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) ⋯)
|
|
(@instCoeHTCTOfCoeHTC
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Nat
|
|
(@instCoeHTCOfCoeOTC
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Nat
|
|
(@instCoeOTCOfCoeOut
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Nat Nat
|
|
(@subtypeCoe Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
|
|
(@instCoeOTC Nat))))
|
|
@instCoeTOfCoeHTCT
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Bool
|
|
(@Subtype.mk Nat (fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
|
|
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) ⋯)
|
|
(@instCoeHTCTOfCoeHTC
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Bool
|
|
(@instCoeHTCOfCoeOTC
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Bool
|
|
(@instCoeOTCOfCoeOut
|
|
(@Subtype Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) Nat
|
|
Bool (@subtypeCoe Nat fun x => @GT.gt Nat instLTNat x (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
|
|
(@instCoeOTCOfCoeTC Nat Bool (@instCoeTCOfCoe_1 Nat Bool natToBool)))))
|
|
@instCoeTOfCoeHTCT Nat (Option Nat) (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
|
|
(@instCoeHTCTOfCoeHTC Nat (Option Nat)
|
|
(@instCoeHTCOfCoeOTC Nat (Option Nat)
|
|
(@instCoeOTCOfCoeTC Nat (Option Nat) (@instCoeTCOfCoe_1 Nat (Option Nat) (@optionCoe Nat)))))
|
|
@instCoeTOfCoeHTCT Bool (Option Nat) true
|
|
(@instCoeHTCTOfCoeHTC Bool (Option Nat)
|
|
(@instCoeHTCOfCoeOTC Bool (Option Nat)
|
|
(@instCoeOTCOfCoeTC Bool (Option Nat)
|
|
(@instCoeTCOfCoe Nat (Option Nat) Bool (@optionCoe Nat) (@instCoeTCOfCoe_1 Bool Nat boolToNat)))))
|
|
@instCoeTOfCoeDep Prop
|
|
(@Eq Nat (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
|
|
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
|
|
Bool
|
|
(@decPropToBool
|
|
(@Eq Nat (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
|
|
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
|
|
(instDecidableEqNat (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
|
|
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
|
|
@instCoeTOfCoeHTCT Bool (Option Nat) true
|
|
(@instCoeHTCTOfCoeHTC Bool (Option Nat)
|
|
(@instCoeHTCOfCoeOTC Bool (Option Nat)
|
|
(@instCoeOTCOfCoeTC Bool (Option Nat)
|
|
(@instCoeTCOfCoe Nat (Option Nat) Bool (@optionCoe Nat) (@instCoeTCOfCoe_1 Bool Nat boolToNat)))))
|