Question: allow overwriting fields that have default values?

[imkiva]

fields that have default values are called FieldImpl in Aya source code. Are we going to allow overwriting the field impls? for example

\struct Cross : \Set
  | base : Nat
  | plus1 => suc base

The plus1 has a value which depends on base. So we can use this syntax to create Cross:

\new Cross { | base => zero }

where the plus1 should be suc zero

Should we allow this new operation ?

\new Cross { | base => zero | plus1 => zero }

I think we should because we will have extends in the future which also overwrites fields. What do you think?

[ice1000]

I just wanna point out one thing -- the order of overwriting should matter. Say, if you wanna overwrite a field, you gotta override it before new fields got added.

[re-xyr]

I think we should establish the dependency between fields and instantiate by that order.

[re-xyr]

Unchangeable fields are semantically identical to mere function definitons so we won't need that (or we have that as a sugar).