From 53c862e34bd372e4bbdcb5fe5ca80c3e4f029928 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Aug 2020 19:15:56 -0700 Subject: [PATCH] chore: add another example using the generated eliminator --- tmp/eqns/prototype2.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tmp/eqns/prototype2.lean b/tmp/eqns/prototype2.lean index a6ae780b60..11378e1480 100644 --- a/tmp/eqns/prototype2.lean +++ b/tmp/eqns/prototype2.lean @@ -678,6 +678,13 @@ elimTest7 _ (fun _ _ => Bool) n xs (fun _ => true) (fun _ _ => false) #eval isSizeOne (Vec.cons 1 Vec.nil) #eval isSizeOne (Vec.cons 2 (Vec.cons 1 Vec.nil)) +def singleton? {n : Nat} (xs : Vec Nat n) : Option Nat := +elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none) + +#eval singleton? Vec.nil +#eval singleton? (Vec.cons 10 Vec.nil) +#eval singleton? (Vec.cons 20 (Vec.cons 10 Vec.nil)) + def ex8 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil))) × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=