chore: move update stage0
This commit is contained in:
parent
13c2a8ff51
commit
e3a982b0fa
374 changed files with 184 additions and 497 deletions
1
stage0/src/Init/Coe.lean
generated
1
stage0/src/Init/Coe.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control.lean
generated
1
stage0/src/Init/Control.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Alternative.lean
generated
1
stage0/src/Init/Control/Alternative.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Applicative.lean
generated
1
stage0/src/Init/Control/Applicative.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Conditional.lean
generated
1
stage0/src/Init/Control/Conditional.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/EState.lean
generated
1
stage0/src/Init/Control/EState.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Except.lean
generated
1
stage0/src/Init/Control/Except.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Functor.lean
generated
1
stage0/src/Init/Control/Functor.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Id.lean
generated
1
stage0/src/Init/Control/Id.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Monad.lean
generated
1
stage0/src/Init/Control/Monad.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/MonadControl.lean
generated
1
stage0/src/Init/Control/MonadControl.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/MonadFunctor.lean
generated
1
stage0/src/Init/Control/MonadFunctor.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/MonadLift.lean
generated
1
stage0/src/Init/Control/MonadLift.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Option.lean
generated
1
stage0/src/Init/Control/Option.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/Reader.lean
generated
1
stage0/src/Init/Control/Reader.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/State.lean
generated
1
stage0/src/Init/Control/State.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Control/StateRef.lean
generated
1
stage0/src/Init/Control/StateRef.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data.lean
generated
1
stage0/src/Init/Data.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array.lean
generated
1
stage0/src/Init/Data/Array.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/Basic.lean
generated
1
stage0/src/Init/Data/Array/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/BinSearch.lean
generated
1
stage0/src/Init/Data/Array/BinSearch.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/ForIn.lean
generated
1
stage0/src/Init/Data/Array/ForIn.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/Macros.lean
generated
1
stage0/src/Init/Data/Array/Macros.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/QSort.lean
generated
1
stage0/src/Init/Data/Array/QSort.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Array/Subarray.lean
generated
1
stage0/src/Init/Data/Array/Subarray.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Basic.lean
generated
1
stage0/src/Init/Data/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/ByteArray.lean
generated
1
stage0/src/Init/Data/ByteArray.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/ByteArray/Basic.lean
generated
1
stage0/src/Init/Data/ByteArray/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Char.lean
generated
1
stage0/src/Init/Data/Char.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Char/Basic.lean
generated
1
stage0/src/Init/Data/Char/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Fin.lean
generated
1
stage0/src/Init/Data/Fin.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Fin/Basic.lean
generated
1
stage0/src/Init/Data/Fin/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Float.lean
generated
1
stage0/src/Init/Data/Float.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/FloatArray.lean
generated
1
stage0/src/Init/Data/FloatArray.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/FloatArray/Basic.lean
generated
1
stage0/src/Init/Data/FloatArray/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Hashable.lean
generated
1
stage0/src/Init/Data/Hashable.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Int.lean
generated
1
stage0/src/Init/Data/Int.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Int/Basic.lean
generated
1
stage0/src/Init/Data/Int/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/List.lean
generated
1
stage0/src/Init/Data/List.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/List/Basic.lean
generated
1
stage0/src/Init/Data/List/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/List/BasicAux.lean
generated
1
stage0/src/Init/Data/List/BasicAux.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/List/Control.lean
generated
1
stage0/src/Init/Data/List/Control.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Nat.lean
generated
1
stage0/src/Init/Data/Nat.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Nat/Basic.lean
generated
1
stage0/src/Init/Data/Nat/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Nat/Bitwise.lean
generated
1
stage0/src/Init/Data/Nat/Bitwise.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Nat/Control.lean
generated
1
stage0/src/Init/Data/Nat/Control.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Nat/Div.lean
generated
1
stage0/src/Init/Data/Nat/Div.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Option.lean
generated
1
stage0/src/Init/Data/Option.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Option/Basic.lean
generated
1
stage0/src/Init/Data/Option/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Option/BasicAux.lean
generated
1
stage0/src/Init/Data/Option/BasicAux.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Option/Instances.lean
generated
1
stage0/src/Init/Data/Option/Instances.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Random.lean
generated
1
stage0/src/Init/Data/Random.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Range.lean
generated
1
stage0/src/Init/Data/Range.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/Repr.lean
generated
1
stage0/src/Init/Data/Repr.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/String.lean
generated
1
stage0/src/Init/Data/String.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/String/Basic.lean
generated
1
stage0/src/Init/Data/String/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/String/Extra.lean
generated
1
stage0/src/Init/Data/String/Extra.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/ToString.lean
generated
1
stage0/src/Init/Data/ToString.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/ToString/Basic.lean
generated
1
stage0/src/Init/Data/ToString/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/ToString/Macro.lean
generated
1
stage0/src/Init/Data/ToString/Macro.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Data/UInt.lean
generated
1
stage0/src/Init/Data/UInt.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Fix.lean
generated
1
stage0/src/Init/Fix.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/LeanInit.lean
generated
1
stage0/src/Init/LeanInit.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System.lean
generated
1
stage0/src/Init/System.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System/FilePath.lean
generated
1
stage0/src/Init/System/FilePath.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System/IO.lean
generated
1
stage0/src/Init/System/IO.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System/IOError.lean
generated
1
stage0/src/Init/System/IOError.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System/Platform.lean
generated
1
stage0/src/Init/System/Platform.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/System/ST.lean
generated
1
stage0/src/Init/System/ST.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/Util.lean
generated
1
stage0/src/Init/Util.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Init/WF.lean
generated
1
stage0/src/Init/WF.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Attributes.lean
generated
1
stage0/src/Lean/Attributes.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/AuxRecursor.lean
generated
1
stage0/src/Lean/AuxRecursor.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Class.lean
generated
1
stage0/src/Lean/Class.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler.lean
generated
1
stage0/src/Lean/Compiler.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/BorrowedAnnotation.lean
generated
1
stage0/src/Lean/Compiler/BorrowedAnnotation.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/ClosedTermCache.lean
generated
1
stage0/src/Lean/Compiler/ClosedTermCache.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/ConstFolding.lean
generated
1
stage0/src/Lean/Compiler/ConstFolding.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/ExportAttr.lean
generated
1
stage0/src/Lean/Compiler/ExportAttr.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/ExternAttr.lean
generated
1
stage0/src/Lean/Compiler/ExternAttr.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR.lean
generated
1
stage0/src/Lean/Compiler/IR.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/Basic.lean
generated
1
stage0/src/Lean/Compiler/IR/Basic.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/Borrow.lean
generated
1
stage0/src/Lean/Compiler/IR/Borrow.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/Boxing.lean
generated
1
stage0/src/Lean/Compiler/IR/Boxing.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/Checker.lean
generated
1
stage0/src/Lean/Compiler/IR/Checker.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/CompilerM.lean
generated
1
stage0/src/Lean/Compiler/IR/CompilerM.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/CtorLayout.lean
generated
1
stage0/src/Lean/Compiler/IR/CtorLayout.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/ElimDeadVars.lean
generated
1
stage0/src/Lean/Compiler/IR/ElimDeadVars.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/EmitC.lean
generated
1
stage0/src/Lean/Compiler/IR/EmitC.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/EmitUtil.lean
generated
1
stage0/src/Lean/Compiler/IR/EmitUtil.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/Format.lean
generated
1
stage0/src/Lean/Compiler/IR/Format.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/FreeVars.lean
generated
1
stage0/src/Lean/Compiler/IR/FreeVars.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/LiveVars.lean
generated
1
stage0/src/Lean/Compiler/IR/LiveVars.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/NormIds.lean
generated
1
stage0/src/Lean/Compiler/IR/NormIds.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/PushProj.lean
generated
1
stage0/src/Lean/Compiler/IR/PushProj.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/RC.lean
generated
1
stage0/src/Lean/Compiler/IR/RC.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/ResetReuse.lean
generated
1
stage0/src/Lean/Compiler/IR/ResetReuse.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
1
stage0/src/Lean/Compiler/IR/SimpCase.lean
generated
1
stage0/src/Lean/Compiler/IR/SimpCase.lean
generated
|
|
@ -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.
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Reference in a new issue