Skip to content
GitLab

Another try at removing strings.length

Merged Michael Sammler requested to merge ci/msammler/length into master

See discussion in !129 (merged) The idea of this version is to have two notations, one which shadows the bad definition Strings.length and the other which shadows the bad Notation List.length, which is bad because it is parsing only.

Edited by Michael Sammler

Merge request reports