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.
31 lines
1.1 KiB
Text
31 lines
1.1 KiB
Text
/-
|
||
Tests for try? integration with solve_by_elim.
|
||
|
||
This tests that `try?` now includes `solve_by_elim` in its pipeline,
|
||
which is a prerequisite for removing the "first pass" solve_by_elim from `apply?`.
|
||
-/
|
||
|
||
set_option autoImplicit true
|
||
|
||
-- Basic hypothesis chaining: solve_by_elim can chain f and g to get from a to γ
|
||
-- This requires more than just `assumption` - it needs to apply f then g
|
||
example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by
|
||
try?
|
||
|
||
-- Multi-step application: needs to apply f four times
|
||
example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 4 := by
|
||
try?
|
||
|
||
-- Backtracking case: needs to find the right combination of hypotheses
|
||
example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
|
||
(a : α) (_ha₁ : P₁ a)
|
||
(a' : α) (ha'₁ : P₁ a') (ha'₂ : P₂ a') : β := by
|
||
try?
|
||
|
||
-- Simple case that could be solved by either assumption or solve_by_elim
|
||
example (h : Nat) : Nat := by
|
||
try?
|
||
|
||
-- Two-argument function application
|
||
example {α β : Type} (f : α → α → β) (a : α) : β := by
|
||
try?
|