Quelle  Record.out   Sprache: unbekannt

{| 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
{| a := 0; b := 0 |}
     : T
fun '{| |} => 0
     : LongModuleName.test -> nat
     = {|
         a :=
           {|
             LongModuleName.long_field_name0 := 0;
             LongModuleName.long_field_name1 := 1;
             LongModuleName.long_field_name2 := 2;
             LongModuleName.long_field_name3 := 3
           |};
         b :=
           fun
             '{|
                LongModuleName.long_field_name0 := a;
                LongModuleName.long_field_name1 := b;
                LongModuleName.long_field_name2 := c;
                LongModuleName.long_field_name3 := d
              |} =>
           (a, b, c, d)
       |}
     : T
     = {|
         a :=
           {|
             long_field_name0 := 0;
             long_field_name1 := 1;
             long_field_name2 := 2;
             long_field_name3 := 3
           |};
         b :=
           fun
             '{|
                long_field_name0 := a;
                long_field_name1 := b;
                long_field_name2 := c;
                long_field_name3 := d
              |} =>
           (a, b, c, d)
       |}
     : T
fun x : R => 0
             +++
             x.(field) 0
     : R -> nat
File "./output/Record.v", line 85, characters 23-24:
The command has indeed failed with message:
Projection f expected 1 explicit parameter.
File "./output/Record.v", line 93, characters 2-40:
Warning:
The record squashed could not be defined as a primitive record because it is
squashed. [non-primitive-record,records,default]
File "./output/Record.v", line 93, characters 30-31:
Warning: x cannot be defined because it is informative and squashed is not.
[cannot-define-projection,records,default]
File "./output/Record.v", line 95, characters 2-31:
Warning:
The record noprojs could not be defined as a primitive record because it has
no projections. [non-primitive-record,records,default]
File "./output/Record.v", line 97, characters 2-48:
Warning:
The record norelevantprojs could not be defined as a primitive record because
it is not in SProp but all projections may be irrelevant.
[non-primitive-record,records,default]
File "./output/Record.v", line 99, characters 2-33:
Warning:
The record anonproj could not be defined as a primitive record because it has
an anonymous projection. [non-primitive-record,records,default]