[Agda] general question

[Martin Escardo]

> syntax bounded-∀ (λ n → a) m = ∀⟨ n < m ⟩→ a
>
> data bounded-∀ (A : ℕ → Set) : ℕ → Set where
> bounded-∀-intro₀ :
> ∀⟨ O < O ⟩→ A O
>
> bounded-∀-intro₁ :
> {m : ℕ} → A m → (∀⟨ n < m ⟩→ A n) → ∀⟨ n < succ m ⟩→ A n

This compiles. But it is better to write


syntax bounded-∀ (λ n → a) m = ∀⟨ n < m ⟩→ a

data bounded-∀ (A : ℕ → Ω) : ℕ → Ω where
   bounded-∀-intro₀ :
     ∀⟨ n < O ⟩→ A n

   bounded-∀-intro₁ : {m : ℕ} →
     A m → (∀⟨ n < m ⟩→ A n) → ∀⟨ n < succ m ⟩→ A n