rocq-prover/stdlib

誰かが対応中かもしれないイシューは最後に並べています。 すべて日付順に表示

• Maintaining NaryFunctions

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#293 · 2026年7月15日 に作成

• deprecating List.nth in favor of List.nth_default

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#243 · 2026年3月4日 に作成

• Importing PeanoNat.Nat shadows eq definition

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#242 · コメント 3 件 · 2026年3月2日 に作成

• Documentation could be automatically deployed

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 25/100

  rocq-prover/stdlib#241 · 2026年2月23日 に作成

• Releasing? (Docker CI images do not support latest stdlib)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#230 · コメント 11 件 · 2026年1月28日 に作成

• Using dune when installing the package

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 42/100

  rocq-prover/stdlib#225 · コメント 2 件 · 2025年11月14日 に作成

• Regression: Importing ZArith leads to setoid_rewrite performance degradation

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 42/100

  rocq-prover/stdlib#200 · コメント 2 件 · 2025年7月23日 に作成

• same html title for all files (stdlib doc)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 42/100

  rocq-prover/stdlib#195 · コメント 2 件 · 2025年7月17日 に作成

• Github CI anomaly zoo

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  rocq-prover/stdlib#168 · コメント 4 件 · 2025年6月7日 に作成

• Design: connecting booleans to their meaning

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#165 · リアクション 1 件 · 2025年6月5日 に作成

• GitHub CI queuing

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  rocq-prover/stdlib#153 · コメント 10 件 · 2025年5月31日 に作成

• Require status checks to pass before merging (for auto-merge, no policy change)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  rocq-prover/stdlib#148 · コメント 3 件 · 2025年5月13日 に作成

• CI: is there a way to see CI-built HTML documentation for an unmerged PR?

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  rocq-prover/stdlib#145 · コメント 1 件 · 2025年5月10日 に作成

• CI jobs should explicitly set the `name` field

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 55/100

  rocq-prover/stdlib#142 · 2025年5月6日 に作成

• "Cachix setup coq" failed on CI

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 25/100

  rocq-prover/stdlib#140 · 2025年5月4日 に作成

• `NoDup_dec` definition is opaque

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 1/5 1時間未満 初心者へのやさしさ 50/100

  rocq-prover/stdlib#125 · 2025年3月31日 に作成

• What is the merging policy for stdlib? (contributing.md is nonsense)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#116 · コメント 2 件 · 2025年3月3日 に作成

• Keep All.v in topological order

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 42/100

  rocq-prover/stdlib#106 · コメント 1 件 · 2025年2月12日 に作成

• `int64` equivalent for `ExtrOcamlIntConv`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#3 · 2024年12月21日 に作成

• stdlib exports conflicting notations

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#4 · 2024年12月20日 に作成

• Confusing warning: Using Vector.t is known to be technically difficult

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#5 · コメント 5 件 · 2024年12月7日 に作成

• ZifyBool overriding zify_post_hook is a bad idea

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  rocq-prover/stdlib#6 · 2024年6月5日 に作成

• Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#7 · コメント 18 件 · 2024年1月3日 に作成

• `Scheme Equality for nat` + `Require Import Coq.Logic.Eqdep_dec.` breaks `inversion` ("Illegal application" at Qed)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#8 · 2023年10月2日 に作成

• Bottlenecks in standard library

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#9 · コメント 1 件 · 2023年7月20日 に作成

• List.rev is unexpectedly quadratic

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 1/5 1時間未満 初心者へのやさしさ 35/100

  rocq-prover/stdlib#10 · コメント 3 件 · 2023年7月12日 に作成

• `ListNotations` breaks primitive array syntax

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#11 · コメント 8 件 · 2023年7月5日 に作成

• Import Nsatz redefines "0" and "1"

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#12 · コメント 6 件 · 2023年5月29日 に作成

• Missing lemmas about Prop: absorbing or neutral elements for various operations

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  rocq-prover/stdlib#14 · コメント 3 件 · 2022年12月14日 に作成

• Setoid rewriting hardcodes stdlib paths instead of relying on Register

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#15 · コメント 1 件 · 2022年11月24日 に作成

• Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#16 · 2022年7月31日 に作成

• coqc infinite loop in type class resolution

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#17 · コメント 8 件 · 2022年6月20日 に作成

• The Standard Library should not be adding transitivity and symmetry hints to `core`

  再び着手できるかも このイシューのプルリクエストはマージされずにクローズされました。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 38/100

  rocq-prover/stdlib#18 · コメント 3 件 · 2022年6月3日 に作成

• Dep_elim database not used?

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#20 · コメント 1 件 · 2022年5月19日 に作成

• `Require Import Coq.Sorting.Permutation.` slows down `rewrite_strat` > 10x

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#21 · コメント 7 件 · 2022年2月17日 に作成

• Strong natural induction should be simpler

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  rocq-prover/stdlib#22 · リアクション 1 件 · 2021年8月10日 に作成

• binary and octal number notations

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  rocq-prover/stdlib#23 · コメント 1 件 · リアクション 1 件 · 2021年5月6日 に作成

• Cannot pattern match on exist in program definitions

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#24 · 2021年4月23日 に作成

• incl_dec and NoDup_dec should be Defined and not Qed

  再び着手できるかも このイシューのプルリクエストはマージされずにクローズされました。 オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 1/5 1〜3時間 初心者へのやさしさ 65/100

  rocq-prover/stdlib#25 · 2021年4月21日 に作成

• btauto should not modify core HintDb

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#27 · コメント 4 件 · 2020年7月14日 に作成

• definition of field and ring theories excluded from standard library reference main page

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 35/100

  rocq-prover/stdlib#28 · コメント 3 件 · リアクション 1 件 · 2020年4月16日 に作成

• Require Import Int63 breaks `Definition land := ...`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 20/100

  rocq-prover/stdlib#29 · コメント 1 件 · リアクション 1 件 · 2020年3月25日 に作成

• NoDup List Cut Function

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#30 · コメント 1 件 · 2020年2月28日 に作成

• Z.mod_mul_r and Z.rem_mul_r reversed

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  rocq-prover/stdlib#31 · 2019年10月30日 に作成

• Reals: Make "Rsqr x" and an alias for "x^2"

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  rocq-prover/stdlib#32 · コメント 17 件 · 2019年9月1日 に作成

• ExtrOCamlInt63 contains an upper-case C in its name

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  rocq-prover/stdlib#33 · コメント 10 件 · 2019年8月26日 に作成

• suprirsing hints leak

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  rocq-prover/stdlib#34 · コメント 4 件 · 2019年7月26日 に作成

• Naming conventions broken (cos/sin)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  rocq-prover/stdlib#35 · コメント 2 件 · 2019年7月8日 に作成

• Please add gprogress and grepeat and gtry and g+ and g[> tac.. ]

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 20/100

  rocq-prover/stdlib#37 · コメント 2 件 · リアクション 1 件 · 2019年3月8日 に作成

• Declare `Hint Mode` for `Reflexive`, `Symmetric`, `Equivalence`, ...

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 38/100

  rocq-prover/stdlib#38 · コメント 9 件 · 2019年1月30日 に作成