agda2scheme icon indicating copy to clipboard operation
agda2scheme copied to clipboard

Published 20 hours ago • verified publisher icon jespercockx

Don't store constructor tag for records and single-constructor datatypes

Open jespercockx opened this issue 3 years ago • 0 comments

Currently constructors always store a tag, even when there is only a single option.

As a stretch goal, we could even skip the constructor tag if there are several constructors, as long as there is only a single constructor of each given arity. We can then just determine which constructor we have by looking at the length of the argument list.

jespercockx avatar May 12 '22 07:05 jespercockx