feat(library/init/lean/parser/term): parse and expand sorry

library/init/lean/expander.lean

@@ -393,6 +393,9 @@ def universes.transform : transformer :=
   let v := view «universes» stx,
   pure $ syntax.list $ v.ids.map (λ id, review «universe» {id := id})
 
+def sorry.transform : transformer :=
+λ stx, pure $ mk_app (glob_id `sorry_ax) [review hole {}, glob_id `bool.ff]
+
 local attribute [instance] name.has_lt_quick
 
 -- TODO(Sebastian): replace with attribute
@@ -410,7 +413,8 @@ def builtin_transformers : rbmap name transformer (<) := rbmap.from_list [
   (declaration.name, declaration.transform),
   (level.leading.name, level.leading.transform),
   (term.subtype.name, subtype.transform),
-  (universes.name, universes.transform)
+  (universes.name, universes.transform),
+  (sorry.name, sorry.transform)
 ] _
 
 structure expander_state :=

library/init/lean/parser/term.lean

@@ -332,6 +332,10 @@ node! inaccessible [".(":max_prec, term: term.parser, ")"]
 def anonymous_inaccessible.parser : term_parser :=
 node! anonymous_inaccessible ["._":max_prec]
 
+@[derive parser.has_tokens parser.has_view]
+def sorry.parser : term_parser :=
+node! «sorry» ["sorry":max_prec]
+
 -- TODO(Sebastian): replace with attribute
 @[derive has_tokens]
 def builtin_leading_parsers : token_map term_parser := token_map.of_list [
@@ -360,7 +364,8 @@ def builtin_leading_parsers : token_map term_parser := token_map.of_list [
   ("{", struct_inst.parser),
   ("{", subtype.parser),
   (".(", inaccessible.parser),
-  ("._", anonymous_inaccessible.parser)
+  ("._", anonymous_inaccessible.parser),
+  ("sorry", sorry.parser)
 ]
 
 @[derive parser.has_tokens parser.has_view]