Open heueristik opened 1 week ago
Request: Allow consistent use of the named syntax.
Context: I defined named function arguments in a trait and the instance
trait type AdditivelyHomomorphic T := mkAdditivelyHomomorphic {add : (v1 : T) -> (v2 : T) -> T}; Property-AdditivelyHomomorphic {T} {{Eq T}} {{AdditivelyHomomorphic T}} (f : T -> T) (v1 v2 : T) : Bool := f (AdditivelyHomomorphic.add v1 v2) == AdditivelyHomomorphic.add (f v1) (f v2);
but couldn't use the named application syntax afterwards. When trying, I got an The identifier AdditivelyHomomorphic.add does not have a type signature with named arguments Error.
The identifier AdditivelyHomomorphic.add does not have a type signature with named arguments
Steps to reproduce:
Request: Allow consistent use of the named syntax.
Context: I defined named function arguments in a trait and the instance
but couldn't use the named application syntax afterwards. When trying, I got an
The identifier AdditivelyHomomorphic.add does not have a type signature with named arguments
Error.Steps to reproduce: