chore: fix tests

This commit is contained in:
Leonardo de Moura 2020-01-28 10:34:27 -08:00
parent 642509229f
commit bb1a90b24d
5 changed files with 3 additions and 5 deletions

View file

@ -18,7 +18,7 @@ partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
-- copied from stdlib, but with `UInt32` indices instead of `Nat` (which is more comparable to the other versions)
abbrev Idx := UInt32
instance : HasLift UInt32 Nat := ⟨UInt32.toNat⟩
prefix `↑`:max := coe
prefix `↑`:max := oldCoe
@[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : αα → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
| as, i, j =>

View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Coe
import Init.Data.Option.Basic
import Init.Data.List.BasicAux
import Init.System.IO

View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Coe
import Init.Data.Option.Basic
import Init.Data.List.BasicAux
import Init.System.IO

View file

@ -1,2 +1,2 @@
def foo (xs : List Nat) :=
xs.span (fun n => coe (decide (n = 1)))
xs.span (fun n => oldCoe (decide (n = 1)))

View file

@ -216,7 +216,7 @@ def three := 3
#eval run "#check g three (z := zero)"
#eval run "open Lean.Parser
@[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
@[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! oldCoe \"hi\"
#check myParser"
#eval run "#check (fun stx => if True then let e := stx; HasPure.pure e else HasPure.pure stx : Nat → Id Nat)"