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

chore: cleanup example

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-13 06:35:20 -07:00
parent 7bb9638ea6
commit 04f071606f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tmp/eqns/matchArrayLit.lean
View file

@ -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