Stream: Coq users

Topic: ✔ Last element of a vector


view this post on Zulip Julin Shaji (Sep 30 2023 at 06:06):

Thanks!

That made it work:

  Definition isLsbSet {n:nat} (v: Bvector n): bool.
  Proof.
    refine (
      match n as m return m <= n -> bool with
      | O => fun _ => false (* There is no LSB *)
      | S n' => fun pf => nth_order v (_:n'<n)
    end _); trivial.
    Show Proof.
  Defined.

view this post on Zulip Notification Bot (Sep 30 2023 at 06:06):

Julin Shaji has marked this topic as resolved.


Last updated: Jun 13 2024 at 19:02 UTC