With the --keep-pattern-variables flag (which is enabled by default nowadays) Agda will not overwrite existing pattern variables with dot patterns, but it might still introduce dot patterns as arguments to an introduced constructor. For example:
{-# OPTIONS --keep-pattern-variables #-}
open import Agda.Builtin.Bool
data Box : Bool → Set where
box : (x : Bool) → Box x
test : Box true → Set
test x = {! x !}
Case splitting produces the pattern test (box .true). Martín Escardó reports on Zulip that his can be confusing for students, especially if they haven't learned about dot patterns (yet).
So the question is: should we also prevent these dot patterns from being generated under --keep-pattern-variables, or should there be a separate flag --no-dot-patterns that completely disables their generation (similar to --no-postfix-projections)? And in the latter case, should this option be enabled by default?
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