Mercurial > urweb

comparison src/coq/Axioms.v @ 618:be88d2d169f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most of expression semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 13:17:06 -0500
parents d26d1f3acfd6
children
comparison
equal deleted inserted replaced
617:5b358e8f9f09 618:be88d2d169f6
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 Require Import Syntax.
29
30 Set Implicit Arguments. 28 Set Implicit Arguments.
31 29
32 30
33 Axiom ext_eq : forall dom ran (f g : forall x : dom, ran x), 31 Axiom ext_eq : forall dom ran (f g : forall x : dom, ran x),
34 (forall x, f x = g x) 32 (forall x, f x = g x)