coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Function : Cannot define graph(s) when it should?

From: "Rui Baptista" <rui.baptista AT mail.com>
To: coq-club AT inria.fr
Cc: "Coq Club" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Function : Cannot define graph(s) when it should?
Date: Sat, 20 Sep 2014 14:54:34 +0200
Importance: normal
Sensitivity: Normal

There is a command for getting a functional induction scheme for functions defined with the "Fixpoint" command.

Functional Scheme

There are also commands for making the arguments of a function implicit after the function has been defined.

Arguments
Set Contextual Implicit
Set Implicit Arguments
Set Maximal Implicit Insertion
Set Reversible Pattern Implicit
Set Strongly Strict Implicit
Unset Strict Implicit

Take a look at the command reference.

http://coq.inria.fr/refman/command-index.html

[Coq-Club] Function : Cannot define graph(s) when it should?, Jonathan, 09/19/2014
- Re: [Coq-Club] Function : Cannot define graph(s) when it should?, Rui Baptista, 09/20/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Function : Cannot define graph(s) when it should?, julien . forest, 09/20/2014