Typed Macros

doc/make/nix.md

@@ -89,7 +89,7 @@ nix run .#HEAD-as-stage0.emacs-dev&
 ```
 To run `nix build` on the second stage outside of the second editor, use
 ```bash
-nix build .#stage0-from-input
+nix build .#stage0-from-input --override-input lean-stage0 .\?rev=$(git rev-parse HEAD)
 ```
 This setup will inadvertently change your `flake.lock` file, which you can revert when you are done.
 

flake.nix

@@ -41,7 +41,9 @@
         };
         tsandebug = tsan.override { debug = true; };
         stage0-from-input = lean-packages.override {
-          stage0 = lean-stage0.packages.${system}.lean;
+          stage0 = pkgs.writeShellScriptBin "lean" ''
+            exec ${lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
+          '';
         };
         inherit self;
       };

src/Init/Coe.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Core
+import Init.Prelude
 
 universe u v w w'
 
@@ -40,7 +40,7 @@ class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
 class CoeSort (α : Sort u) (β : outParam (Sort v)) where
   coe : α → β
 
-syntax:max (name := coeNotation) "↑" term:max : term
+syntax:1024 (name := coeNotation) "↑" term:1024 : term
 
 instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where
   coe a := Coe.coe (CoeTC.coe a : β)
@@ -81,18 +81,18 @@ instance coeSortToCoeTail [inst : CoeSort α β] : CoeTail α β where
 /- Basic instances -/
 
 @[inline] instance boolToProp : Coe Bool Prop where
-  coe b := b = true
+  coe b := Eq b true
 
 instance boolToSort : CoeSort Bool Prop where
-  coe b := b = true
+  coe b := Eq b true
 
 instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
   coe := decide p
 
 instance optionCoe {α : Type u} : CoeTail α (Option α) where
   coe := some
 
-instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α where
+instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead (Subtype p) α where
   coe v := v.val
 
 /- Coe bridge -/
@@ -105,7 +105,7 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
 -- Helper definition used by the elaborator. It is not meant to be used directly by users
 @[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
   let a ← x
-  pure <| CoeT.coe a
+  pure (CoeT.coe a)
 
 instance [CoeFun α β] (a : α) : CoeDep α a (β a) where
   coe := CoeFun.coe a

src/Init/Conv.lean

@@ -54,7 +54,9 @@ macro "erw " s:rwRuleSeq : conv => `(rw (config := { transparency := Meta.Transp
 macro "args" : conv => `(congr)
 macro "left" : conv => `(lhs)
 macro "right" : conv => `(rhs)
-macro "intro " xs:(colGt ident)* : conv => `(ext $xs*)
+syntax "intro " (colGt ident)* : conv
+macro_rules
+  | `(conv| intro $[$xs:ident]*) => `(conv| ext $xs*)
 
 syntax enterArg := ident <|> group("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv

src/Init/Data/Format/Syntax.lean

@@ -44,4 +44,7 @@ def formatStx (stx : Syntax) (maxDepth : Option Nat := none) (showInfo := false)
 instance : ToFormat (Syntax) := ⟨formatStx⟩
 instance : ToString (Syntax) := ⟨@toString Format _ ∘ format⟩
 
+instance : ToFormat (TSyntax k) := ⟨(format ·.raw)⟩
+instance : ToString (TSyntax k) := ⟨(toString ·.raw)⟩
+
 end Lean.Syntax

src/Init/Data/Option/Basic.lean

@@ -34,9 +34,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none,   _ => none
   | some a, b => b a
 
-@[inline] protected def map (f : α → β) (o : Option α) : Option β :=
-  Option.bind o (some ∘ f)
-
 @[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
   if let some a := o then
     return some (← f a)