From 04f071606f12e31b0ce98efb803cd5dc7c51cec9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Mar 2020 06:35:20 -0700 Subject: [PATCH] chore: cleanup example --- tmp/eqns/matchArrayLit.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tmp/eqns/matchArrayLit.lean b/tmp/eqns/matchArrayLit.lean index becfeff1c8..349ccbf588 100644 --- a/tmp/eqns/matchArrayLit.lean +++ b/tmp/eqns/matchArrayLit.lean @@ -142,11 +142,11 @@ def matchArrayLit {α : Type u} (C : Array α → Sort v) (a : Array α) (h₄ : ∀ a, C a) : C a := if h : a.size = 0 then - @Eq.ndrec _ _ C (h₁ ()) _ (toArrayLitEq a 0 h).symm + @Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (toArrayLitEq a 0 h).symm else if h : a.size = 1 then - @Eq.ndrec _ _ C (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 1 h).symm + @Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 1 h).symm else if h : a.size = 3 then - @Eq.ndrec _ _ C (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 3 h).symm + @Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 3 h).symm else h₄ a