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

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

Interaction between tactics and instance search · Issue #4777 · agda/agda · GitHub

Instance search does speculative type checking of the available candidates for an instance goal. This can involve running tactics (as happened in #4593). I suspect in most cases you don't want this, but I can imagine there might be exceptions.

Some options:

1. Never run tactics during instance search
2. Provide a function to abort a tactic if invoked during instance search
3. Status quo
4. ??

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