lean2/tests/lean/elab_bug1.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
  Set: lean::pp::implicit
let P : ℕ → Bool := λ x : ℕ, @neq ℕ x 0, Q : ∀ x : ℕ, P (x + 1) := λ x : ℕ, Nat::succ_nz x in Q :
    ∀ x : ℕ, (λ x : ℕ, @neq ℕ x 0) (x + 1)
-												fix(library/elaborator): in optimization for metavariable free terms

The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-01-23 02:03:08 +00:00
+								  Set: pp::colors
 								  Set: pp::unicode
 								  Set: lean::pp::implicit
 								let P : ℕ → Bool := λ x : ℕ, @neq ℕ x 0, Q : ∀ x : ℕ, P (x + 1) := λ x : ℕ, Nat::succ_nz x in Q :
 								    ∀ x : ℕ, (λ x : ℕ, @neq ℕ x 0) (x + 1)