UlfNorell
commented
10 years ago From andreas....@gmail.com on November 23, 2013 09:40:06
Ulf, that could have been caused by your improved printing for lhss.
Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Defect Highlighting Priority-High Milestone-2.3.4 HiddenArguments Display
From vitus...@gmail.com on November 23, 2013 03:22:43
module DotPatterns where
data ℕ : Set where zero : ℕ suc : ℕ → ℕ
data T : ℕ → Set where t : ∀ n → T (suc n)
dot₁ : ∀ {n} → T n → ℕ dot₁ .{n = suc x} (t x) = zero
dot₂ : ∀ n → T n → ℕ dot₂ .(suc x) (t x) = zero
dot₃ : ∀ {n} → T n → ℕ dot₃ .{suc x} (t x) = zero
Dotted patterns of both dot₂ and dot₃ generate hyperlinks with class="DottedPattern InductiveConstructor" (for f) and "DottedPattern Bound" (for x), while dotted pattern of dot₁ has just class="InductiveConstructor" and class="Bound", respectively.
This behaviour seems to have changed in the last week: roughly a week old version of Agda generates correct HTML for dot₁, the development version (as of Nov 22) does not.
Original issue: http://code.google.com/p/agda/issues/detail?id=976