max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-10 07:43:01 -07:00
parent 394d49da58
commit 7553dc12c0
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/986.lean.expected.out
View file

@ -4,7 +4,7 @@
(h : Nat.succ j' < Array.size a),
Array.insertionSort.swapLoop lt a (Nat.succ j') h =
let_fun h' := (_ : j' < Array.size a);
if lt (getElem a (Nat.succ j') h) (getElem a j' h') = true then
if lt a[Nat.succ j'] a[j'] = true then
Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j'
(_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
else a

8
tests/lean/infoTree.lean.expected.out
View file

@ -297,13 +297,13 @@
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
Array.push (getElem! s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabApp
getElem! s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ @ «_aux_Init_Util___macroRules_term__[_]_!_1»
Array.push s.snd[1]! s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabApp
s.snd[1]! : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ @ «_aux_Init_Util___macroRules_term__[_]_!_1»
Macro expansion
s.2[1]!
===>
getElem!✝ s.2 1
getElem! s.snd 1 : Array Nat @ ⟨28, 2⟩†-⟨28, 7⟩ @ Lean.Elab.Term.elabApp
s.snd[1]! : Array Nat @ ⟨28, 2⟩†-⟨28, 7⟩ @ Lean.Elab.Term.elabApp
[.] `getElem!._@.infoTree._hyg.139 : none @ ⟨28, 2⟩†-⟨28, 9⟩†
@getElem! : {Cont Idx Elem : Type} →
{Dom : Cont → Idx → Prop} →
@ -315,7 +315,7 @@
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩
1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩ @ Lean.Elab.Term.elabNumLit
[.] getElem! s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ : some Array.{0} Nat
[.] s.snd[1]! : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ : some Array.{0} Nat
@Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 10⟩-⟨28, 14⟩
s.fst : Nat @ ⟨28, 15⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabProj
[.] `s : some ?_uniq.1071 @ ⟨28, 15⟩-⟨28, 16⟩