<div dir="ltr"><div class="gmail_quote"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Dear Agda Community,<br><br>When I attempt to unquote a declaration where a `Name` is not provided, but instead created using `freshName`,<div>the resulting function is not in scope. I want to create functions based on lists of terms, so the option of passing</div><div>in names is not ideal.</div><div><br></div><div>Here is the current scenerario ---a minimal example is below, and attached.<br><br><div><div>{- Works, but is undesirable }</div><div>unquoteDecl identity = ⋯make the identity function⋯</div><div><br></div><div>{- Desirable but "identity" is not in scope. -}</div><div>unquoteDecl = do η ← freshName "identity"</div><div>                 ⋯make the identity function⋯</div></div><div><br></div>Moreover, regarding reflection is it possible to unquote a datatype or a record declaration?</div><div>Does anyone have any documentation on how to use the /current/,<br>or a /recent/, version of Agda's reflection mechanism.</div><div>( My personal notes can be found here: <br>   <a href="https://github.com/alhassy/gentle-intro-to-reflection" target="_blank">https://github.com/alhassy/gentle-intro-to-reflection</a> )<br><br>Best regards,<br><br>Musa Al-hassy<br><br><div>------------------------------------------------------------------------</div><div>module tangled where</div><div><br></div><div>open import Relation.Binary.PropositionalEquality hiding ([_])</div><div>open import Data.List as List</div><div>open import Reflection</div><div>open import Data.Nat</div><div>open import Data.Unit</div><div><br></div><div>_>>=_        : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B</div><div>_>>=_ = bindTC</div><div>_>>_        : ∀ {a b} {A : Set a} {B : Set b} → TC A → TC B → TC B</div><div>_>>_  = λ p q → p >>= (λ _ → q)</div><div><br></div><div>{- 𝓋isible 𝓇elevant 𝒶rgument -}</div><div>𝓋𝓇𝒶 : {A : Set} → A → Arg A</div><div>𝓋𝓇𝒶 = arg (arg-info visible relevant)</div><div><br></div><div>unquoteDecl</div><div>  = do η ← freshName "identity"</div><div>       τ ← quoteTC (∀ {A : Set} → A → A)</div><div>       declareDef (𝓋𝓇𝒶 η) τ</div><div>       defineFun η [ clause [ 𝓋𝓇𝒶 (var "x") ] (var 0 []) ]</div><div><br></div><div>{-</div><div>-- “identity” is not in scope!?</div><div>_ : ∀ {x : ℕ}  →  identity x  ≡  x</div><div>_ = refl</div><div>-}<br></div><div><br></div></div></div></div></div></div>
</div></div>