Don't emit primitive records for recursive single-constructor inductives

dumps/rec_single_ctor

@@ -0,0 +1,293 @@
+1 #NS 0 RecInd
+2 #NS 1 mk
+3 #NS 0 A
+4 #NS 0 u
+1 #UP 4
+0 #ES 1
+5 #NS 0 a
+6 #NS 5 _@
+7 #NS 6 dumps
+8 #NS 7 rec_single_ctor
+9 #NS 8 _hyg
+10 #NI 9 6
+1 #EV 0
+11 #NI 9 8
+2 #EC 1 1
+3 #EV 1
+4 #EA 2 3
+5 #EV 2
+6 #EA 2 5
+7 #EP #BD 11 4 6
+8 #EP #BD 10 1 7
+9 #EP #BI 3 0 8
+2 #US 0
+3 #UM 2 1
+10 #ES 3
+11 #EP #BD 3 0 10
+#IND 1 1 11 1 2 9 4
+12 #NS 0 Eq
+13 #NS 12 refl
+14 #NS 0 α
+15 #NS 0 u_1
+4 #UP 15
+12 #ES 4
+13 #EC 12 4
+14 #EA 13 3
+15 #EA 14 1
+16 #EA 15 1
+17 #EP #BD 5 1 16
+18 #EP #BI 14 12 17
+16 #NS 6 Init
+17 #NS 16 Prelude
+18 #NS 17 _hyg
+19 #NI 18 194
+20 #NI 18 196
+19 #ES 0
+20 #EP #BD 20 3 19
+21 #EP #BD 19 1 20
+22 #EP #BI 14 12 21
+#IND 2 12 22 1 13 18 15
+21 #NS 1 casesOn
+22 #NS 0 motive
+23 #NS 0 t
+23 #EA 2 1
+24 #EP #BD 23 23 12
+24 #NS 0 mk
+25 #EV 3
+26 #EA 2 25
+27 #EC 2 1
+28 #EV 4
+29 #EA 27 28
+30 #EA 29 3
+31 #EA 30 1
+32 #EA 25 31
+33 #EP #BD 11 26 32
+34 #EP #BD 10 5 33
+35 #EA 5 3
+36 #EP #BD 24 34 35
+37 #EP #BD 23 4 36
+38 #EP #BI 22 24 37
+39 #EP #BI 3 0 38
+25 #NS 1 rec
+40 #EC 25 4 1
+41 #EA 40 25
+42 #EA 41 5
+43 #EA 2 28
+26 #NS 0 a_ih
+27 #NS 26 _@
+28 #NS 27 dumps
+29 #NS 28 rec_single_ctor
+30 #NS 29 _hyg
+31 #NI 30 8
+44 #EA 28 1
+45 #EA 25 5
+46 #EA 45 3
+47 #EL #BD 31 44 46
+48 #EL #BD 11 43 47
+49 #EL #BD 10 25 48
+50 #EA 42 49
+51 #EA 50 3
+52 #EL #BD 24 34 51
+53 #EL #BD 23 4 52
+54 #EL #BI 22 24 53
+55 #EL #BI 3 0 54
+#DEF 21 39 55 15 4
+32 #NS 12 ndrec
+33 #NS 0 u2
+5 #UP 33
+56 #ES 5
+34 #NI 18 212
+35 #NS 0 u1
+6 #UP 35
+57 #ES 6
+58 #EP #BD 34 3 57
+36 #NS 0 m
+59 #EA 1 3
+37 #NS 0 b
+38 #NS 0 h
+60 #EC 12 5
+61 #EA 60 28
+62 #EA 61 25
+63 #EA 62 1
+64 #EA 25 3
+65 #EP #BD 38 63 64
+66 #EP #BI 37 25 65
+67 #EP #BD 36 59 66
+68 #EP #BI 22 58 67
+69 #EP #BI 5 1 68
+70 #EP #BI 14 56 69
+39 #NS 12 rec
+71 #EC 39 6 5
+72 #EV 5
+73 #EA 71 72
+74 #EA 73 28
+40 #NS 0 x
+41 #NS 40 _@
+42 #NS 41 Init
+43 #NS 42 Prelude
+44 #NS 43 _hyg
+45 #NI 44 225
+46 #NI 44 224
+75 #EV 6
+76 #EA 60 75
+77 #EA 76 72
+78 #EA 77 1
+79 #EA 72 3
+80 #EL #BD 46 78 79
+81 #EL #BD 45 72 80
+82 #EA 74 81
+83 #EA 82 5
+84 #EA 83 3
+85 #EA 84 1
+86 #EL #BD 38 63 85
+87 #EL #BI 37 25 86
+88 #EL #BD 36 59 87
+89 #EL #BI 22 58 88
+90 #EL #BI 5 1 89
+91 #EL #BI 14 56 90
+#DEF 32 70 91 35 33
+47 #NS 0 rfl
+92 #EC 12 1
+93 #EA 92 3
+94 #EA 93 1
+95 #EA 94 1
+96 #EP #BI 5 1 95
+97 #EP #BI 14 0 96
+98 #EC 13 1
+99 #EA 98 3
+100 #EA 99 1
+101 #EL #BI 5 1 100
+102 #EL #BI 14 0 101
+#DEF 47 97 102 4
+48 #NS 12 symm
+103 #EA 92 5
+104 #EA 103 3
+105 #EA 104 1
+106 #EA 92 25
+107 #EA 106 3
+108 #EA 107 5
+109 #EP #BD 38 105 108
+110 #EP #BI 37 3 109
+111 #EP #BI 5 1 110
+112 #EP #BI 14 0 111
+113 #EC 39 0 1
+114 #EA 113 25
+115 #EA 114 5
+49 #NI 44 285
+50 #NS 38 _@
+51 #NS 50 Init
+52 #NS 51 Prelude
+53 #NS 52 _hyg
+54 #NI 53 286
+116 #EA 92 28
+117 #EA 116 25
+118 #EA 117 1
+119 #EA 92 72
+120 #EA 119 3
+121 #EA 120 28
+122 #EL #BD 54 118 121
+123 #EL #BD 49 25 122
+124 #EA 115 123
+125 #EC 47 1
+126 #EA 125 25
+127 #EA 126 5
+128 #EA 124 127
+129 #EA 128 3
+130 #EA 129 1
+131 #EL #BD 38 105 130
+132 #EL #BI 37 3 131
+133 #EL #BI 5 1 132
+134 #EL #BI 14 0 133
+#DEF 48 112 134 4
+55 #NS 1 eta
+135 #EC 1 4
+136 #EA 135 1
+7 #UM 2 4
+137 #EC 12 7
+138 #EA 135 3
+139 #EA 137 138
+140 #EC 2 4
+141 #EA 140 3
+142 #EJ 1 0 1
+143 #EA 141 142
+144 #EJ 1 1 1
+145 #EA 143 144
+146 #EA 139 145
+147 #EA 146 1
+148 #EP #BD 40 136 147
+149 #EP #BI 3 12 148
+150 #EC 21 0 4
+151 #EA 150 3
+56 #NS 23 _@
+57 #NS 56 dumps
+58 #NS 57 rec_single_ctor
+59 #NS 58 _hyg
+60 #NI 59 63
+152 #EA 135 5
+153 #EA 137 152
+154 #EA 153 3
+155 #EA 154 1
+156 #EA 135 25
+157 #EA 137 156
+158 #EA 140 25
+159 #EJ 1 0 5
+160 #EA 158 159
+161 #EJ 1 1 5
+162 #EA 160 161
+163 #EA 157 162
+164 #EA 163 5
+165 #EP #BD 38 155 164
+166 #EL #BD 60 138 165
+167 #EA 151 166
+168 #EA 167 1
+61 #NI 10 64
+62 #NI 11 65
+63 #NS 50 dumps
+64 #NS 63 rec_single_ctor
+65 #NS 64 _hyg
+66 #NI 65 66
+169 #EA 157 5
+170 #EA 158 3
+171 #EA 170 1
+172 #EA 169 171
+173 #EC 32 0 7
+174 #EA 135 28
+175 #EA 173 174
+176 #EA 140 28
+177 #EA 176 5
+178 #EA 177 3
+179 #EA 175 178
+180 #EA 135 72
+181 #EA 137 180
+182 #EA 140 72
+183 #EA 182 142
+184 #EA 183 144
+185 #EA 181 184
+186 #EA 185 1
+187 #EL #BD 40 174 186
+188 #EA 179 187
+189 #EC 13 7
+190 #EA 189 174
+191 #EJ 1 0 178
+192 #EA 176 191
+193 #EJ 1 1 178
+194 #EA 192 193
+195 #EA 190 194
+196 #EA 188 195
+197 #EA 196 25
+198 #EC 48 7
+199 #EA 198 174
+200 #EA 199 25
+201 #EA 200 178
+202 #EA 201 1
+203 #EA 197 202
+204 #EL #BD 66 172 203
+205 #EL #BD 62 152 204
+206 #EL #BD 61 3 205
+207 #EA 168 206
+208 #EA 189 138
+209 #EA 208 1
+210 #EA 207 209
+211 #EL #BD 40 136 210
+212 #EL #BI 3 12 211
+#DEF 55 149 212 15

dumps/rec_single_ctor.lean

@@ -0,0 +1,8 @@
+inductive RecInd.{u} (A : Sort u)
+  | mk : A → RecInd A → RecInd A
+
+-- Definitional eta does NOT hold for RecInd
+-- Propositional eta
+theorem RecInd.eta (x : RecInd A) : RecInd.mk x.1 x.2 = x := by
+  fail_if_success rfl
+  cases x; rfl