Modal bindings are not shown in the goal context

banacorn / agda-mode-vscode

agda-mode on VS Code

MIT License

169 stars 39 forks source link

Closed plt-amy closed 9 months ago

plt-amy commented 1 year ago

module FlatScope where

data Flat (@♭ A : Set) : Set where
  flat : (@♭ a : A) → Flat A

flat′ : {@♭ A : Set} (@♭ a : A) → Flat A
flat′ x = {!   !}

banacorn commented 9 months ago

Thanks!!!!