chore: remove #lang lean4 header

2020-10-25 09:49:14 -07:00 · 2020-10-25 09:49:14 -07:00 · 13c2a8ff51
commit 13c2a8ff51
parent e67076ada8
314 changed files with 0 additions and 314 deletions
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control.lean
+++ b/src/Init/Control.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Alternative.lean
+++ b/src/Init/Control/Alternative.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Applicative.lean
+++ b/src/Init/Control/Applicative.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Conditional.lean
+++ b/src/Init/Control/Conditional.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Functor.lean
+++ b/src/Init/Control/Functor.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) Luke Nelson and Jared Roesch. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Monad.lean
+++ b/src/Init/Control/Monad.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) Luke Nelson and Jared Roesch. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/MonadControl.lean
+++ b/src/Init/Control/MonadControl.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/MonadFunctor.lean
+++ b/src/Init/Control/MonadFunctor.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/MonadLift.lean
+++ b/src/Init/Control/MonadLift.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/BinSearch.lean
+++ b/src/Init/Data/Array/BinSearch.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/ForIn.lean
+++ b/src/Init/Data/Array/ForIn.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/Macros.lean
+++ b/src/Init/Data/Array/Macros.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Basic.lean
+++ b/src/Init/Data/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/ByteArray.lean
+++ b/src/Init/Data/ByteArray.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Char.lean
+++ b/src/Init/Data/Char.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Fin.lean
+++ b/src/Init/Data/Fin.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/FloatArray.lean
+++ b/src/Init/Data/FloatArray.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Int.lean
+++ b/src/Init/Data/Int.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Nat.lean
+++ b/src/Init/Data/Nat.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Nat/Bitwise.lean
+++ b/src/Init/Data/Nat/Bitwise.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Nat/Control.lean
+++ b/src/Init/Data/Nat/Control.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Option.lean
+++ b/src/Init/Data/Option.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Option/BasicAux.lean
+++ b/src/Init/Data/Option/BasicAux.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Option/Instances.lean
+++ b/src/Init/Data/Option/Instances.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Random.lean
+++ b/src/Init/Data/Random.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Range.lean
+++ b/src/Init/Data/Range.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/String.lean
+++ b/src/Init/Data/String.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/ToString.lean
+++ b/src/Init/Data/ToString.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/ToString/Macro.lean
+++ b/src/Init/Data/ToString/Macro.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Fix.lean
+++ b/src/Init/Fix.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System.lean
+++ b/src/Init/System.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System/FilePath.lean
+++ b/src/Init/System/FilePath.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System/IOError.lean
+++ b/src/Init/System/IOError.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System/Platform.lean
+++ b/src/Init/System/Platform.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler.lean
+++ b/src/Lean/Compiler.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/BorrowedAnnotation.lean
+++ b/src/Lean/Compiler/BorrowedAnnotation.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/ClosedTermCache.lean
+++ b/src/Lean/Compiler/ClosedTermCache.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/ConstFolding.lean
+++ b/src/Lean/Compiler/ConstFolding.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR.lean
+++ b/src/Lean/Compiler/IR.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/CtorLayout.lean
+++ b/src/Lean/Compiler/IR/CtorLayout.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/ElimDeadVars.lean
+++ b/src/Lean/Compiler/IR/ElimDeadVars.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/EmitUtil.lean
+++ b/src/Lean/Compiler/IR/EmitUtil.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/PushProj.lean
+++ b/src/Lean/Compiler/IR/PushProj.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/ResetReuse.lean
+++ b/src/Lean/Compiler/IR/ResetReuse.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@ -1,4 +1,3 @@
-#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
--- a/Show more
+++ b/Show more