From ab2ee0390ddf5b5aa4e6150c3b73101afa114374 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Nov 2020 10:19:14 -0800 Subject: [PATCH] chore: fix tests --- tests/lean/mvar3.lean | 2 +- tests/lean/namelit.lean.expected.out | 16 ++++++++-------- tests/lean/run/constantCompilerBug.lean | 4 ++-- tests/lean/run/unif_issue.lean | 4 ++-- .../syntaxInNamespacesAndPP.lean.expected.out | 4 ++-- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean index aa699db01b..77033e4d43 100644 --- a/tests/lean/mvar3.lean +++ b/tests/lean/mvar3.lean @@ -86,7 +86,7 @@ def mctx6 := R2.1 #print "assigning ?m1 and ?n.1" def R3 := let mctx := mctx6.assignExpr `m3 x; -let mctx := mctx.assignExpr (mkNameNum `n 1) (mkLambda `_ bi typeE natE); +let mctx := mctx.assignExpr (Name.mkNum `n 1) (mkLambda `_ bi typeE natE); -- ?n.2 is instantiated because we have the delayed assignment `?n.2 α x := ?m1` (mctx.instantiateMVars e2) def e3 := R3.1 diff --git a/tests/lean/namelit.lean.expected.out b/tests/lean/namelit.lean.expected.out index b2ee2fe64a..54caade097 100644 --- a/tests/lean/namelit.lean.expected.out +++ b/tests/lean/namelit.lean.expected.out @@ -1,8 +1,8 @@ -Lean.mkNameStr Lean.Name.anonymous "foo" : Lean.Name -Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "foo") "bla" : Lean.Name -Lean.mkNameStr Lean.Name.anonymous "foo bla" : Lean.Name -Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "foo bla") "hello world" : Lean.Name -Lean.mkNameStr (Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name -Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "foo") "hello" : Lean.Name -Lean.mkNameStr Lean.Name.anonymous "hello" : Lean.Name -Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "hello") "world !!!" : Lean.Name +Lean.Name.mkStr Lean.Name.anonymous "foo" : Lean.Name +Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "bla" : Lean.Name +Lean.Name.mkStr Lean.Name.anonymous "foo bla" : Lean.Name +Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "hello world" : Lean.Name +Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name +Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "hello" : Lean.Name +Lean.Name.mkStr Lean.Name.anonymous "hello" : Lean.Name +Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "hello") "world !!!" : Lean.Name diff --git a/tests/lean/run/constantCompilerBug.lean b/tests/lean/run/constantCompilerBug.lean index 04d800930e..df2f6cb9d8 100644 --- a/tests/lean/run/constantCompilerBug.lean +++ b/tests/lean/run/constantCompilerBug.lean @@ -6,9 +6,9 @@ open Lean open Lean.Parser def regBlaParserAttribute : IO Unit := -registerBuiltinDynamicParserAttribute (mkNameSimple "blaParser") (mkNameSimple "bla") +registerBuiltinDynamicParserAttribute (Name.mkSimple "blaParser") (Name.mkSimple "bla") @[inline] def parser : Parser := -categoryParser (mkNameSimple "bla") 0 +categoryParser (Name.mkSimple "bla") 0 #check @parser diff --git a/tests/lean/run/unif_issue.lean b/tests/lean/run/unif_issue.lean index 3f2d6dc3b2..7d2632eb42 100644 --- a/tests/lean/run/unif_issue.lean +++ b/tests/lean/run/unif_issue.lean @@ -8,7 +8,7 @@ open Lean let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing; let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing; let discr_2 : _ := a; - ite (Lean.Syntax.isOfKind discr_2 (Lean.mkNameStr (Lean.mkNameStr (Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "Lean") "Parser") "Term") "add")) + ite (Lean.Syntax.isOfKind discr_2 (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Lean") "Parser") "Term") "add")) (let discr_3 : _ := Lean.Syntax.getArg discr_2 0; let discr_4 : _ := Lean.Syntax.getArg discr_2 1; let discr_5 : _ := Lean.Syntax.getArg discr_2 2; @@ -27,7 +27,7 @@ open Lean let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing; let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing; let discr_2 : _ := a; - ite (Lean.Syntax.isOfKind discr_2 (Lean.mkNameStr (Lean.mkNameStr (Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "Lean") "Parser") "Term") "add")) + ite (Lean.Syntax.isOfKind discr_2 (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Lean") "Parser") "Term") "add")) (let discr_3 : _ := Lean.Syntax.getArg discr_2 0; let discr_4 : _ := Lean.Syntax.getArg discr_2 1; let discr_5 : _ := Lean.Syntax.getArg discr_2 2; diff --git a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out index ee4f844999..f07ede733b 100644 --- a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out +++ b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out @@ -19,6 +19,6 @@ bla true [Elab.app.finalize] after etaArgs, true : Bool [Elab.command] end def Bla.bla : Lean.ParserDescr := -Lean.ParserDescr.node (Lean.mkNameStr (Lean.mkNameStr Lean.Name.anonymous "Bla") "bla") 1023 +Lean.ParserDescr.node (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Bla") "bla") 1023 (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol "bla") - (Lean.ParserDescr.cat (Lean.mkNameStr Lean.Name.anonymous "term") 0)) + (Lean.ParserDescr.cat (Lean.Name.mkStr Lean.Name.anonymous "term") 0))