Ssreflect Users Discussion List

[Georges Gonthier <>]

  Implicit arguments are not less robust than ML polymorphism. You can use 
the @ notation to turn them off for a given application (say, a partial 
application), and you can reassign the Implicit status if you don't like the 
one the automatic heuristic came up with.

-- Georges

-----Original Message-----
From:  []
Sent: 04 July 2008 12:19
To: 
Subject: Delimit Implicit Arguments?

Hello.

Is there a way to set Implicit Arguments so that it only takes effect
when unresolved wildcards are generalized (ssr's behavior),
but does not when they generate a type error outright (Coq's behavior)?

Concretely, I want the following script to work,
without setting Implicit Arguments.

Variable a : nat.
Variable g: nat -> nat -> nat.
Variable p: nat -> Prop.

Axiom f_p: forall a1 a2, p a1 -> p a2 -> p (g a1 2).

Goal p a ->True.
 move => pa.
 have:= f_p pa.

This ML-like generalization would make my tactic script robust
against minor modifications of axioms,
which I often do for better structuring the script;
it is attractive for me to decrease the potential of painful bugs,
but I do not want to use Implicit Arguments otherwise,
since it could make the script fragile.

With best,
Keiko