1
1
mirror of https://github.com/anoma/juvix.git synced 2024-11-30 14:13:27 +03:00
juvix/tests/positive/Records2.juvix
Łukasz Czajka 3030196fdd Non-recursive definitions (#3138)
* Closes #2968 
* Implements detection of function-like definitions, which either:
  - have some arguments on the left of `:`, or
  - have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```
2024-11-04 18:18:39 +01:00

15 lines
231 B
Plaintext

module Records2;
import Stdlib.Data.Nat open;
type Pair (A B : Type) :=
mkPair {
pfst : A;
psnd : B
};
main : Pair Nat Nat :=
let
p : Pair Nat Nat := mkPair 2 2;
in p@Pair{pfst := Pair.pfst p + Pair.psnd p};