Anonymous module printed in goal

[GoogleCodeExporter]

When playing around with Issue #632 I discovered this

data Bool : Set where
  false true : Bool

record Foo (b : Bool) : Set where
  field
    _*_ : Bool → Bool → Bool

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

horror1 : (F : Foo false) (x : Bool) → let open Foo F in _*_ x ≡ (λ x → x)
horror1 F x = {!!} -- Goal: (F .Issue632._.* x) x ≡ (λ x₁ → x₁)

Shouldn't the printer expand definitions with anonymous qualifiers?

Original issue reported on code.google.com by andreas....@gmail.com on 20 Oct 2012 at 2:52

[GoogleCodeExporter]

Problem: loops in the presence of displayForms

-- LOOPS
horror3 : (F : Foo false) → let open Foo F in (x : Bool) → _*_ x ≡ (λ x → x)
horror3 F x = x -- {!!} -- Goal: (F .Issue632._.* x) ≡ (λ x₁ → x₁)
  where open Foo F

displayForm unexpands the definition again, so we are looping.

Original comment by andreas....@gmail.com on 20 Oct 2012 at 5:10

[GoogleCodeExporter]

Fixed by not expand definitions that were introduced by displayForms.

Original comment by andreas....@gmail.com on 20 Oct 2012 at 7:17

• Changed state: Fixed
• Added labels: Display
• Removed labels: Printing

[GoogleCodeExporter]

Issue #644 has been merged into this issue.

Original comment by andreas....@gmail.com on 20 Oct 2012 at 7:50