blob: d45343fe60d72fd5d0d782a1247c881f45888bd2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
{| field := 5 |}
: test
{| field := 5 |}
: test
{| field_r := 5 |}
: test_r
build_c 5
: test_c
build 5
: test
build 5
: test
{| field_r := 5 |}
: test_r
build_c 5
: test_c
fun '(C _ p) => p
: N -> True
fun '{| T := T |} => T
: N -> Type
fun '(C T p) => (T, p)
: N -> Type * True
fun '{| q := p |} => p
: M -> True
fun '{| U := T |} => T
: M -> Type
fun '{| U := T; q := p |} => (T, p)
: M -> Type * True
fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
|
