From b74ab91d1db4b1b88471fc47460b6be15a58b162 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Apr 2006 21:15:27 +0000 Subject: [PATCH] exported pp function for terms --- helm/software/matita/library/legacy/coq.ma | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma index d3c74fe21..76da7d898 100644 --- a/helm/software/matita/library/legacy/coq.ma +++ b/helm/software/matita/library/legacy/coq.ma @@ -56,3 +56,7 @@ interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinition interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)). +interpretation "Coq's natural 'not less or equal than'" + 'nleq x y = (cic:/Coq/Init/Logic/not.con + (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)). + -- 2.39.2