New namespacing of inductive types #16

dannypsnl commented 2026年05月15日 03:06:20 +02:00

1. By default will not expose constructor, e.g. zero, to top-level, but put it under Nat/zero
2. If expected type is Nat, it will try to find name in it, so zero in this case will refer to Nat/zero
3. open clause for top-level let definition

close #10

1. By default will not expose constructor, e.g. `zero`, to top-level, but put it under `Nat/zero` 2. If expected type is `Nat`, it will try to find name in it, so `zero` in this case will refer to `Nat/zero` 3. `open` clause for top-level `let` definition close #10