Andreas Abel

> it's very strange that Agda accepts the following: I think this is the OP.

> it _is_ possible if you name the enclosing modules, and open them afterwards I don't think it is. Isn't it funny that no one can tell who modules behave...

I doubt I have the capacity to fix this for 2.8.0.

This checks, WTF? ```agda import Agda.Builtin.Nat as M using () import Agda.Builtin.Nat as N using (Nat) import Agda.Builtin.Nat as Z using (zero) import Agda.Builtin.Nat as S using (suc) open M...

I put the original example into an online confluence checker, [CONFident](http://zenon.dsic.upv.es/confident/): ``` (VAR n m) (RULES plus(suc(n),m) -> suc(plus(n,m)) plus(n,suc(m)) -> suc(plus(n,m)) ) ``` It reports critical pair `` and...

Yeah, sorry for the fundamental critique, research is always preliminary... But I am still puzzled that there is no better criterion than the triangle property after decades of research into...

Rebased onto current master (2.6.5).

Too late for 2.7.

See also: - #7903

> I suspect that the feature was designed in this way. Note, however, that it does sometimes work with explicit tactic arguments, e.g. here: https://github.com/agda/agda/blob/6c6b5c929677dd81f89e7ae4952f1b3a64fc0533/test/Succeed/TacticModality.agda#L28-L33 My opinion is that `f...