sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: fix tests

Browse Source
This commit is contained in:
Leonardo de Moura
2020-05-26 14:54:27 -07:00
parent f820341430
commit 17b6957f6c
31 changed files with 35 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
tests/compiler/expr.lean
View File

@@ -1,4 +1,4 @@
import Lean.Expr
import Lean
open Lean
def main : IO UInt32 :=

2
tests/compiler/termparsertest1.lean
View File

@@ -1,4 +1,4 @@
import Lean.Parser.Term
import Lean
open Lean
open Lean.Parser

2
tests/lean/PPRoundtrip.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Elab
open Lean.Elab.Term

2
tests/lean/StxQuot.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
namespace Lean
open Lean.Elab

2
tests/lean/ctor_layout.lean
View File

@@ -3,7 +3,7 @@ open Lean
open Lean.IR
def tst : IO Unit :=
do env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}];
do env ← importModules [{module := `Lean.Compiler.IR.Basic}];
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";

2
tests/lean/mvar_fvar.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
#eval (mkFVar `a).hasFVar

2
tests/lean/run/111.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
new_frontend
open Lean
#check mkNullNode -- Lean.Syntax

2
tests/lean/run/Reparen.lean
View File

@@ -39,7 +39,7 @@ let (debug, f) : Bool × String := match args with
| [f] => (false, f)
| _ => panic! "usage: file [-d]";
initSearchPath none;
env ← importModules [{module := `Init.Lean.Parser}];
env ← importModules [{module := `Lean.Parser}];
stx ← Lean.Parser.parseFile env args.head!;
let header := stx.getArg 0;
some s ← pure header.reprint | throw $ IO.userError "header reprint failed";

2
tests/lean/run/closure1.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Meta

2
tests/lean/run/constantCompilerBug.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
new_frontend

2
tests/lean/run/eval_unboxed_const.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
def c1 : Bool := true

2
tests/lean/run/evalconst.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
def x := 10

2
tests/lean/run/foldConsts.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
def mkTerm : Nat → Expr

2
tests/lean/run/generalizeTelescope.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Meta

2
tests/lean/run/genindices.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
universe u

4
tests/lean/run/instances.lean
View File

@@ -1,9 +1,9 @@
import Init.Lean
import Lean
open Lean
open Lean.Meta
def tst1 : IO Unit :=
do let mods := [`Init.Lean];
do let mods := [`Lean];
env ← importModules $ mods.map $ fun m => {module := m};
let insts := env.getGlobalInstances;
IO.println (format insts);

2
tests/lean/run/instuniv.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
def tst : IO Unit :=

2
tests/lean/run/kernel1.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean

2
tests/lean/run/kernel2.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
def checkDefEq (a b : Name) : MetaIO Unit := do

2
tests/lean/run/kevin.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
new_frontend
open Lean

8
tests/lean/run/meta1.lean
View File

@@ -107,10 +107,10 @@ mkLet `a (mkSort levelOne) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVa
#eval tstInferType [`Init.Core] $ mkLit (Literal.strVal "hello")
#eval tstInferType [`Init.Core] $ mkMData {} $ mkLit (Literal.natVal 10)
#eval tstInferType [`Init.Lean.Util.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstInferType [`Init.Lean.Util.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstWHNF [`Init.Lean.Util.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstWHNF [`Init.Lean.Util.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstInferType [`Lean.Util.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstInferType [`Lean.Util.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
#eval tstWHNF [`Lean.Util.Trace] (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))
#eval tstWHNF [`Lean.Util.Trace] (mkProj `Lean.TraceState 0 (mkProj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])))
def t10 : Expr :=
let nat := mkConst `Nat [];

2
tests/lean/run/replace.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean

2
tests/lean/run/structure.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
structure S1 :=

2
tests/lean/run/termElab.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Elab

2
tests/lean/run/termParserAttr.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Elab

2
tests/lean/run/toExpr.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean

2
tests/lean/run/unif_issue.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
#eval toString $

2
tests/lean/run/unif_issue2.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
new_frontend

2
tests/playground/reelab.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Elab
open Lean.Elab.Term

2
tests/playground/termParserAttr.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean
open Lean.Elab

2
tests/plugin/SnakeLinter.lean
View File

@@ -1,4 +1,4 @@
import Init.Lean
import Lean
open Lean