Search results

Long Qed in <code>examples/std/int_to_Zp.v</code>

Status: Open.

#47 In rocq-community/trocq;

· t6s opened on May 19, 2025

Examples of CoqEAL style refinement

Status: Open.

#40 In rocq-community/trocq;

· palmskog opened on Jan 16, 2025

Automated class inference fault when using <code>Trocq Use</code>

bugSomething isn't workingSomething isn't working

UIUser interface of the pluginUser interface of the plugin

Status: Open.

#32 In rocq-community/trocq;

· ecranceMERCE opened on Jan 23, 2024

Predicate naming in constraint graph

documentationImprovements or additions to documentationImprovements or additions to documentation

invalidThis doesn't seem rightThis doesn't seem right

Status: Open.

#31 In rocq-community/trocq;

· ecranceMERCE opened on Jan 19, 2024

Duplicate code getting parametricity classes

documentationImprovements or additions to documentationImprovements or additions to documentation

invalidThis doesn't seem rightThis doesn't seem right

Status: Open.

#30 In rocq-community/trocq;

· ecranceMERCE opened on Jan 19, 2024

Adapt and use HB to generate Trocq relational structures

dependenciesCompatibility with other packagesCompatibility with other packages

enhancementNew feature or requestNew feature or request

Status: Open.

#28 In rocq-community/trocq;

· CohenCyril opened on Jan 18, 2024

Control in the <code>trocq</code> tactic

enhancementNew feature or requestNew feature or request

UIUser interface of the pluginUser interface of the plugin

Status: Open.

#27 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024

Trocq command opening goals

enhancementNew feature or requestNew feature or request

UIUser interface of the pluginUser interface of the plugin

Status: Open.

#26 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024

Trocq records for inductive types

enhancementNew feature or requestNew feature or request

theoryTheoretical aspects of the pluginTheoretical aspects of the plugin

Status: Open.

#25 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024

Combinator creating full parametricity witnesses from individual record fields

enhancementNew feature or requestNew feature or request

Status: Open.

#24 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024

Syntactic parametricity class search

questionFurther information is requestedFurther information is requested

Status: Open.

#23 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024

Suspension in implementation of weakening

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#22 In rocq-community/trocq;

· ecranceMERCE opened on Jan 18, 2024