Stream: Coq users

Topic: ✔ Program Fixpoint measure - simple example

view this post on Zulip Nikola Katić (Aug 13 2022 at 10:10):

@Paolo Giarrusso thanks for the feedback :smile:
In case someone else (new to this) comes accross a similar problem here is the rest: 

Next Obligation.
  destruct n as [|n'].
  - discriminate.
  - apply (Nat.div_lt _ 256) ; lia.
Qed.

view this post on Zulip Notification Bot (Aug 13 2022 at 10:14):

Nikola Katić has marked this topic as resolved.

view this post on Zulip Nikola Katić (Aug 14 2022 at 14:31):

After adding decreasing fuel argument, everything was straightforward... Closing this topic :check:

view this post on Zulip Notification Bot (Aug 14 2022 at 14:31):

Nikola Katić has marked this topic as resolved.

Last updated: Jan 27 2023 at 02:04 UTC