Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/6783 below:

`@tactic` does not kick in for lambdas · Issue #6783 · agda/agda · GitHub

open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  A : Set

super-tac : Term → TC ⊤
super-tac hole = unify hole (lit (nat 101))

bar = λ {@(tactic super-tac) n : Nat} → n + n

_ : bar ≡ 202
_ = refl

Failed to solve the following constraints:
  _n_40 + _n_40 = 202 : Nat (blocked on _n_40)

In contrast, this works:

bar' : {@(tactic super-tac) n : Nat} → Nat
bar' {n} = n + n

_ : bar' ≡ 202
_ = refl

Maybe tactics in lambdas are silently dropped!?

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4