ndcroos
ndcroos
I will wait for an OK by the maintainers before doing anything. There is also `fast_done` in Coq-Std++. https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v?ref_type=heads#L45 ``` (** [done] can get slow as it calls "trivial". [fast_done]...
Hi, can I work on this, please?
Hi, I'd like to work on this issue. I see the following comment in test_template.py: ``` # Hilbert Schmidt templates take a quantum tape as a parameter. # Therefore unsuitable...
Thanks for your helpful feedback, @jespercockx. I am trying to define Rational: ```agda {-# OPTIONS --no-auto-inline #-} module Haskell.Prim.Rational where open import Haskell.Prim.Integer -------------------------------------------------- -- Definition -- | Rational numbers,...
Hi, can you assign this issue to me, please?
Hi, I'd like to work on this issue, please.
@Alizter A definition of `cyclic` as the cokernel of the multiplication map seems to be already present in `Cyclic.v` here: https://github.com/HoTT/Coq-HoTT/blob/f367ba9002fdd1d6b2ed076ac158f515c99edf45/theories/Algebra/AbGroups/Cyclic.v#L78 I also can't find the cokernel definition in `AbGroups/Z.v`...
@jdchristensen you can post the proof in a comment. I have the following: ```coq Definition ab_mul_cyclic_in (n : nat) (x y : abgroup_Z) : ab_mul y (@cyclic_in n x) =...
@Alizter * in item 1, 'compute definitionally' means something of the form `:= ... .` ? * in item 2, are you sure this should be `cyclic` and not `cyclic'`?
@Alizter for item 1, I have for the first line: `snrapply Build_GroupHomomorphism.` Is this correct?