Ssreflect Users Discussion List

[Vincent Siles <>]

Dear everyone,
I'm wondering if anyone already encountered the following problem and
how to deal with it "in a nice way":
I have a fully formalized program within ssreflect, which doesn't rely
on any axioms. I can even compute
with it within Coq.

However, "Print Assumptions" will return

Axioms:
card : forall T : finType, mem_pred T -> nat
cardEdef : card = (fun (T : finType) (mA : mem_pred T) => size (enum_mem mA))
Finite.EnumDef.enum : forall cT : finType, seq cT
Finite.EnumDef.enumDef : Finite.enum =
                         (fun cT : finType =>
                          Finite.mixin_enum (Finite.class cT))


I know that this follows the following scheme:
Axiom A : foo.
Axiom Adef : A = <actual code of A>.

Is there a "standard" reference to this design choice I can point to so that
any reviewer can be convinced that my work does not actually rely on
any axioms ?

Cheers,
Vincent