mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
4a6a7e6540
- Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ``` |
||
---|---|---|
.. | ||
Base.hs | ||
Options.hs |