Commit 87dd6771 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Use Coq stdlib definitions and lemmas; breaks Coqine

parent 35836cd9
Fixpoint leb (n1 n2 : nat) :=
match n1, n2 with
| O, _ => true
| S _, O => false
| S m1, S m2 => leb m1 m2
end.
......@@ -21,19 +21,19 @@ FOCALIZEC_OPT += -no-coq-code
# We have to generate all dks coming from coq at the same time
# so that universe consistency can be checked globally
COQMODULES = CoqNaturals Peano NPeano List sieve
COQMODULES = Peano NPeano List sieve
VOS = $(V_FILES:.v=.vo)
sieve.vo: CoqNaturals.vo
.PHONY: dks_from_coqine
dks_from_coqine: $(VOS)
../../coqine.sh $(COQMODULES) | $(COQTOP)
CoqNaturals.dk: dks_from_coqine
Coq__Numbers__Natural__Peano__NPeano.dk: dks_from_coqine
Coq__Lists__List.dk: dks_from_coqine
sieve.dk: dks_from_coqine
sieve.dko: CoqNaturals.dko
sieve.dko: CoqNaturals.dko Coq__Numbers__Natural__Peano__NPeano.dko Coq__Lists__List.dko
$(ART_FILES): %.art:
$(OPENTHEORY) info $* &> /dev/null || $(OPENTHEORY) install $*
......@@ -45,7 +45,7 @@ depend: .depend
# Dependencies between .sk.zv files are missing in FOCALIZEDEP
grep '.fo' $@ | sed 's/\.fo/.sk.zv/g' >> $@
natural_coq.sk: CoqNaturals.dko
natural_coq.sk: Coq__Numbers__Natural__Peano__NPeano.dko
natural_hol.sk: HolNaturals.dko
-include .depend
......
......@@ -234,7 +234,7 @@ species CoqLe =
logical let le(m : coq_nat, n : coq_nat) = internal bool
external
| dedukti -> {* cbool_to_bool(CoqNaturals.leb m n) *}
| dedukti -> {* cbool_to_bool(Coq__Numbers__Naturals__Peano__NPeano.leb m n) *}
| coq -> {* *};
proof of le_zero_n = dedukti proof definition of le, zero
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment