Stream: Coq users

Topic: full_fill condition


view this post on Zulip zohaze (May 06 2023 at 06:14):

Fixpoint f (0: nat) (l: list nat) : nat :=
 match l with
 | nil => 0
 | h::t => if 0 <? h then f h t
                     else f 0 t
 end.
goal1: h= f 0 t.
goal2: 0<h.

Last updated: Jun 18 2024 at 10:02 UTC