Lean boot

library/init/lean/elaborator.lean

@@ -27,7 +27,7 @@ namespace elaborator
 -- TODO(Sebastian): should be its own monad?
 structure name_generator :=
 («prefix» : name)
-(next_idx : nat) -- TODO(Sebastian): uint32
+(next_idx : uint32)
 
 structure section_var :=
 (uniq_name : name)
@@ -277,9 +277,15 @@ def to_pexpr : syntax → elaborator_m expr
   | @inaccessible := do
     let v := view inaccessible stx,
     expr.mk_annotation `innaccessible <$> to_pexpr v.term  -- sic
+  | @borrowed := do
+    let v := view borrowed stx,
+    expr.mk_annotation `borrowed <$> to_pexpr v.term
   | @number := do
     let v := view number stx,
     pure $ expr.lit $ literal.nat_val v.to_nat
+  | @string_lit := do
+    let v := view string_lit stx,
+    pure $ expr.lit $ literal.str_val (v.value.get_or_else "NOT_A_STRING")
   | @choice := do
     last::rev ← list.reverse <$> args.mmap (λ a, to_pexpr a)
       | error stx "ill-formed choice",

library/init/lean/parser/term.lean

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