Search results

EclecticLib.v --> Tactic failure: resersible in 1st order mode

Status: Open.

#135 In sifive/Kami;

· nanoeng opened on Dec 8, 2021

Make command fails with Coq 8.12.1

Status: Open.

#134 In sifive/Kami;

· vaishnavi08 opened on Sep 14, 2021

Replace Coq.Fin.t types with Evan's Fin.t types

Status: Open.

#130 In sifive/Kami;

· llee454 opened on Apr 28, 2020

Replace TraceInclusion with TraceInclusion which removes null-steps.

enhancementNew feature or requestNew feature or request

Status: Open.

#129 In sifive/Kami;

· tjmach opened on Apr 27, 2020

Create Tagged Union data type

Status: Open.

#128 In sifive/Kami;

· llee454 opened on Apr 25, 2020

discharge_wf destructs hypotheses on non-wf goals

Status: Open.

#19 In sifive/Kami;

· andres-erbsen-sifive opened on Aug 2, 2019

feature request: bool/prop hypthesis canonicalization

Status: Open.

#18 In sifive/Kami;

· andres-erbsen-sifive opened on Jul 30, 2019

How to prove <code>NoDup</code> in name-parametrized modules?

Status: Open.

#14 In sifive/Kami;

· andres-erbsen-sifive opened on Jul 26, 2019

Consider to use FIRRTL instead of the Verilog

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#11 In sifive/Kami;

· XVilka opened on Jun 14, 2019