Closed leissa closed 1 year ago
In addition: Some more porting from const Def* -> Ref.
Is there an easy rule for when to use Ref
and when to use Def
(const Def*
)?
E.g. should a plugin developer
const Def*
Ref
const Def*
except for normalizers?In addition: Some more porting from const Def* -> Ref.
Is there an easy rule for when to use
Ref
and when to useDef
(const Def*
)? E.g. should a plugin developer* always use `const Def*` * always use `Ref` * use `const Def*` except for normalizers?
The rule is to always use Ref
instead of const Def*
. For everything else such as Def*
or const App*
or Sigma*
, use these types instead.
As I've already pointed out several times the name nominal is confusing as nominals are in fact not nominal as they are tested like structurals for alpha-equiv.
This patch renames:
In the future I'd like to add the option to make mutables truely nominal/unique.
In addition: Some more porting from
const Def*
->Ref
.