Search results

Port Coq code to use done tactic instead of easy and benchmark

help wanted

Status: Open.

#128 In rocq-community/math-classes;

· palmskog opened on Jul 9, 2024

Please suggest example file for Coq Platform "smoke test kit"

Status: Open.

#106 In rocq-community/math-classes;

· MSoegtropIMC opened on Sep 24, 2021

RingOrder for types with decidable equality

Status: Open.

#99 In rocq-community/math-classes;

· mdgeorge4153 opened on May 31, 2021

Use universe polymorphism to eliminate ua_subalgebraT.v

help wanted

Status: Open.

#66 In rocq-community/math-classes;

· spitters opened on Nov 17, 2018

Autogenerate dependency graphs, documentation with travis

Status: Open.

#62 In rocq-community/math-classes;

· spitters opened on Aug 24, 2018

Fix inner product space laws

Status: Open.

#49 In rocq-community/math-classes;

· langston-barrett opened on Mar 29, 2018

notation overwrite warnings

Status: Open.

#47 In rocq-community/math-classes;

· vzaliva opened on Nov 25, 2017

Is there a Decision procedure for ≤ on Rationals?

Status: Open.

#31 In rocq-community/math-classes;

· langston-barrett opened on Feb 10, 2017

Why does rationals_le use the concrete type nat?

Status: Open.

#30 In rocq-community/math-classes;

· langston-barrett opened on Feb 10, 2017

canonical_names.v overwrites a lot of standard notation

Status: Open.

#28 In rocq-community/math-classes;

· langston-barrett opened on Feb 4, 2017