Skip to content

Commit bc449e4

Browse files
augustepoirouxaugustepoiroux
committed
Fix test v4.24.0-rc1
1 parent b8de0d2 commit bc449e4

File tree

1 file changed

+29
-27
lines changed

1 file changed

+29
-27
lines changed

‎test/extract_declaration.expected.out‎

Lines changed: 29 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -302,24 +302,24 @@
302302
"pp":
303303
" := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ",
304304
"constants":
305-
["ParserDescr.cat._@._hyg.202",
306-
"ParserDescr.symbol._@._hyg.202",
307-
"ParserDescr.binary._@._hyg.202",
308-
"ParserDescr.trailingNode._@._hyg.202"]},
305+
["ParserDescr.binary._@.3937598925._hygCtx._hyg.4",
306+
"ParserDescr.trailingNode._@.3937598925._hygCtx._hyg.4",
307+
"ParserDescr.symbol._@.3937598925._hygCtx._hyg.4",
308+
"ParserDescr.cat._@.3937598925._hygCtx._hyg.4"]},
309309
"type":
310310
{"range":
311311
{"synthetic": true,
312312
"start": {"line": 35, "column": 0},
313313
"finish": {"line": 35, "column": 32}},
314314
"pp": " Lean.TrailingParserDescr ",
315-
"constants": ["Lean.TrailingParserDescr._@._hyg.202"]},
315+
"constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]},
316316
"signature":
317317
{"range":
318318
{"synthetic": true,
319319
"start": {"line": 35, "column": 0},
320320
"finish": {"line": 35, "column": 32}},
321321
"pp": " : Lean.TrailingParserDescr ",
322-
"constants": ["Lean.TrailingParserDescr._@._hyg.202"]},
322+
"constants": ["Lean.TrailingParserDescr._@.3937598925._hygCtx._hyg.4"]},
323323
"scope":
324324
{"varDecls": ["variable {α : Type u}"],
325325
"openDecl": [],
@@ -332,10 +332,10 @@
332332
"start": {"line": 35, "column": 0},
333333
"finish": {"line": 35, "column": 32}},
334334
"pp":
335-
" @[ scoped term_parser 1000 ] meta def «term_≋_» : Lean.TrailingParserDescr := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ",
335+
" @[ scoped term_parser 1000 ] public meta def «term_≋_» : Lean.TrailingParserDescr := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ",
336336
"name": "«term_≋_»",
337337
"modifiers":
338-
{"visibility": "regular",
338+
{"visibility": "public",
339339
"recKind": "default",
340340
"isUnsafe": false,
341341
"isProtected": false,
@@ -353,25 +353,25 @@
353353
"pp":
354354
" := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ",
355355
"constants":
356-
["rhs._@._hyg.199",
357-
"throw._@._hyg.221",
358-
"Lean.Macro.Exception.unsupportedSyntax._@._hyg.221",
356+
["[email protected]._hygCtx._hyg.9",
357+
"[email protected]._hygCtx._hyg.3",
359358
"BEq.beq",
360-
"lhs._@._hyg.199"]},
359+
"[email protected]._hygCtx._hyg.3",
360+
"[email protected]._hygCtx._hyg.9"]},
361361
"type":
362362
{"range":
363363
{"synthetic": true,
364364
"start": {"line": 35, "column": 0},
365365
"finish": {"line": 35, "column": 32}},
366366
"pp": " Macro ",
367-
"constants": ["Macro._@._hyg.221"]},
367+
"constants": ["Macro._@.3937598925._hygCtx._hyg.9"]},
368368
"signature":
369369
{"range":
370370
{"synthetic": true,
371371
"start": {"line": 35, "column": 0},
372372
"finish": {"line": 35, "column": 32}},
373373
"pp": " : Macro ",
374-
"constants": ["Macro._@._hyg.221"]},
374+
"constants": ["Macro._@.3937598925._hygCtx._hyg.9"]},
375375
"scope":
376376
{"varDecls": ["variable {α : Type u}"],
377377
"openDecl": [],
@@ -384,16 +384,16 @@
384384
"start": {"line": 35, "column": 0},
385385
"finish": {"line": 35, "column": 32}},
386386
"pp":
387-
" @[ macro Demo.«term_≋_» ] meta def «_aux___macroRules_Demo_term_≋__1» : Macro := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ",
387+
" @[ scoped macro Demo.«term_≋_» ] public meta def «_aux___macroRules_Demo_term_≋__1» : Macro := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ",
388388
"name": "«_aux___macroRules_Demo_term_≋__1»",
389389
"modifiers":
390-
{"visibility": "regular",
390+
{"visibility": "public",
391391
"recKind": "default",
392392
"isUnsafe": false,
393393
"isProtected": false,
394394
"docString": null,
395395
"computeKind": "meta",
396-
"attributes": ["macro Demo.«term_≋_»"]},
396+
"attributes": ["scoped macro Demo.«term_≋_»"]},
397397
"kind": "definition",
398398
"fullName": "Demo.«_aux___macroRules_Demo_term_≋__1»",
399399
"binders": null},
@@ -405,26 +405,28 @@
405405
"pp":
406406
" := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
407407
"constants":
408-
["rhs._@._hyg.199",
409-
"throw._@._hyg.201",
410-
"_@._hyg.201",
411-
"withRef._@._hyg.201",
412-
"f._@._hyg.201",
413-
"lhs._@._hyg.199"]},
408+
["throw._@.3937598925._hygCtx._hyg.4",
409+
"f._@.3937598925._hygCtx._hyg.4",
410+
"lhs._@.3937598925._hygCtx._hyg.3",
411+
"_@.3937598925._hygCtx._hyg.4",
412+
"rhs._@.3937598925._hygCtx._hyg.3",
413+
"withRef._@.3937598925._hygCtx._hyg.4"]},
414414
"type":
415415
{"range":
416416
{"synthetic": true,
417417
"start": {"line": 35, "column": 0},
418418
"finish": {"line": 35, "column": 32}},
419419
"pp": " Lean.PrettyPrinter.Unexpander ",
420-
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]},
420+
"constants":
421+
["[email protected]._hygCtx._hyg.4"]},
421422
"signature":
422423
{"range":
423424
{"synthetic": true,
424425
"start": {"line": 35, "column": 0},
425426
"finish": {"line": 35, "column": 32}},
426427
"pp": " : Lean.PrettyPrinter.Unexpander ",
427-
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]},
428+
"constants":
429+
["[email protected]._hygCtx._hyg.4"]},
428430
"scope":
429431
{"varDecls": ["variable {α : Type u}"],
430432
"openDecl": [],
@@ -437,10 +439,10 @@
437439
"start": {"line": 35, "column": 0},
438440
"finish": {"line": 35, "column": 32}},
439441
"pp":
440-
" @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
442+
" @[ scoped app_unexpander BEq.beq ] public meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
441443
"name": "_aux___unexpand_BEq_beq_1",
442444
"modifiers":
443-
{"visibility": "regular",
445+
{"visibility": "public",
444446
"recKind": "default",
445447
"isUnsafe": false,
446448
"isProtected": false,

0 commit comments

Comments
 (0)