Search results

Align finmap with mathcomp releases?

Status: Open.

#129 In math-comp/finmap;

· hoheinzollern opened on Apr 25, 2025

update the github description by removing the mention to generic sets?

documentation

Status: Open.

#115 In math-comp/finmap;

· affeldt-aist opened on Dec 2, 2024

Missing coercion from finSet to finType

Status: Open.

#102 In math-comp/finmap;

· rhz opened on Nov 18, 2022

Need <code>Coq.Program.Tactics.</code>

Status: Open.

#85 In math-comp/finmap;

· corwin-of-amber opened on Sep 27, 2021

Notation issues for <code>imfset</code>

Status: Open.

#73 In math-comp/finmap;

· chdoc opened on Aug 25, 2020

Add finmap to Coq's CI

Status: Open.

#65 In math-comp/finmap;

· anton-trunov opened on Apr 6, 2020

Fset of a fintype

Status: Open.

#55 In math-comp/finmap;

· Nemeras opened on Jun 26, 2019

Should "unit_irrelevance" fact be moved elsewhere?

Status: Open.

#28 In math-comp/finmap;

· anton-trunov opened on Sep 11, 2018

Simplification in imset2 should be locked

Status: Open.

#26 In math-comp/finmap;

· hivert opened on Aug 29, 2018

Order-preserving morphisms

Status: Open.

#16 In math-comp/finmap;

· ejgallego opened on Nov 6, 2017

Bad notations interaction

Status: Open.

#11 In math-comp/finmap;

· strub opened on Feb 2, 2017

Some finmap/multiset lemmas that might be useful

Status: Open.

#4 In math-comp/finmap;

· mituharu opened on May 28, 2016