max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/run/listex2): fix issue at travis, profiler option is not available in single thread build

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-07 10:39:57 -08:00
parent 94f16d1e44
commit b0bcb4af57
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/listex2.lean
View file

@ -63,7 +63,7 @@ begin [smt]
repeat {ematch} -- It will loop if there is a matching loop
end
set_option profiler true
-- set_option profiler true
/- Smaller problems can be solved using superposition in a reasonable amount of time. -/
example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::l₁ ++ [c] :=