Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / coq-community/trocq issues and pull requests

#38 - fix link to univalent parametricity in README.md

Pull Request - State: open - Opened by chenson2018 7 months ago

#37 - Duplicate link in README.md

Issue - State: open - Opened by chenson2018 7 months ago - 1 comment

#36 - Better examples about reduction modulo p

Pull Request - State: closed - Opened by CohenCyril 11 months ago

#35 - Example with refinements

Pull Request - State: open - Opened by ecranceMERCE about 1 year ago - 1 comment

#34 - Finer-grained hierarchy for list

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#33 - :sparkles: Proofs for list and Empty

Pull Request - State: closed - Opened by ecranceMERCE about 1 year ago

#32 - Automated class inference fault when using `Trocq Use`

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: bug, UI

#31 - Predicate naming in constraint graph

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: documentation, invalid

#30 - Duplicate code getting parametricity classes

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: documentation, invalid

#29 - :memo: Doc on do-not-fail

Pull Request - State: closed - Opened by ecranceMERCE about 1 year ago

#28 - Adapt and use HB to generate Trocq relational structures

Issue - State: open - Opened by CohenCyril about 1 year ago
Labels: enhancement, dependencies

#27 - Control in the `trocq` tactic

Issue - State: open - Opened by ecranceMERCE about 1 year ago - 1 comment
Labels: enhancement, UI

#26 - Trocq command opening goals

Issue - State: open - Opened by ecranceMERCE about 1 year ago - 1 comment
Labels: enhancement, UI

#25 - Trocq records for inductive types

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: enhancement, theory

#24 - Combinator creating full parametricity witnesses from individual record fields

Issue - State: open - Opened by ecranceMERCE about 1 year ago - 1 comment
Labels: enhancement

#23 - Syntactic parametricity class search

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: question

#22 - Suspension in implementation of weakening

Issue - State: open - Opened by ecranceMERCE about 1 year ago
Labels: documentation

#21 - Interaction of the `trocq` tactic with Coq

Issue - State: open - Opened by ecranceMERCE about 1 year ago - 2 comments
Labels: question

#20 - Suboptimal subtyping relation?

Issue - State: open - Opened by ecranceMERCE about 1 year ago - 1 comment
Labels: question, theory

#19 - Generic coercion code

Pull Request - State: open - Opened by CohenCyril about 1 year ago - 3 comments

#18 - WIP: decorrelates knowing translations from using translations

Pull Request - State: open - Opened by CohenCyril about 1 year ago - 1 comment

#17 - Fix comments and example

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#16 - Compress

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#15 - fix

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#14 - generic DOI

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#13 - example of transfer of nat_rec to an abtract type + bugfix

Pull Request - State: closed - Opened by CohenCyril about 1 year ago - 1 comment

#12 - Replacing almost all locate in Hierarchy.v + refactoring

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#11 - Automatic weakening of constants

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#10 - Remove tactic param in favor of trocq

Pull Request - State: closed - Opened by CohenCyril about 1 year ago

#9 - preparing Trocq to add prop

Pull Request - State: open - Opened by CohenCyril about 1 year ago - 1 comment

#8 - :construction: Additional example relating tuples and vectors

Pull Request - State: closed - Opened by ecranceMERCE about 1 year ago - 1 comment

#7 - Support Trakt-like declarations for goal pre-processing

Issue - State: open - Opened by palmskog about 1 year ago - 2 comments
Labels: enhancement, UI

#6 - Adding helper functions

Pull Request - State: closed - Opened by CohenCyril over 1 year ago

#5 - adding relevant cachix

Pull Request - State: closed - Opened by CohenCyril over 1 year ago

#4 - Depending on regular Coq-ELPI

Issue - State: open - Opened by palmskog over 1 year ago
Labels: dependencies

#3 - Setup nix action

Pull Request - State: closed - Opened by CohenCyril over 1 year ago

#2 - update meta data

Pull Request - State: closed - Opened by CohenCyril over 1 year ago - 8 comments

#1 - update files + nix + header < 80char

Pull Request - State: closed - Opened by CohenCyril over 1 year ago