When using automatic proof search in version 2.6.5-a445e3b, adding qualified names from unopened modules as hints doesn't do anything.
postulate A : Set
module M where
postulate a : A
x : A
x = {! M.a !} -- No solution found
open M
y : A
y = {! M.a !} -- works
Running auto in the first hole results in "No solution found" but works in the second hole. Auto works in the first hole when using version 2.6.4.1.
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