In Coq, how do I define a function implicitly, not using Fixedpoint?
For example, define the square root function by f(x)^2 = x.
I looked at the definition of sqrt in std, but it’s a parameter of a module. Do I need a module to define it? I tried:
Module Type Foo. Parameter Inline bubba : nat -> nat. Axiom bubba_spec: forall a, bubba(a) * bubba(a) = a. End Foo.
But I can neither
(I get that this definition doesn’t work for the natural numbers, I’m curious what the error message is, also I can fix it up once I get the basic syntax working.)