Commit bad00f9d authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Split the core/arith directory in 4 subdirectories

parent 5c63b86f
include ../../.config_vars
include ../../Makefile.rules
SUBDIRS = definitions morphisms theorems transfer
TARGETS=all clean install uninstall
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../logic
$(TARGETS):
for d in $(SUBDIRS); do \
$(MAKE) $@ -C $$d || exit 1; \
done
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend $(FCL_FILES:.fcl=.sk)
.PHONY: $(TARGETS)
include ../../../.config_vars
include ../../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../../logic
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled .depend
......@@ -37,8 +37,35 @@ species NatCase =
<1>f conclude;
end;;
species NatOne =
inherit NatCase;
let one = succ(zero);
theorem one_spec : one = succ(zero)
proof = by definition of one;
end;;
species NatBinary =
inherit NatCase;
signature bit0 : Self -> Self;
signature bit1 : Self -> Self;
property bit0_zero : bit0(zero) = zero;
property bit0_succ : all n : Self, bit0(succ(n)) = succ(succ(bit0(n)));
property bit1_spec : all n : Self, bit1(n) = succ(bit0(n));
end;;
species NatPred =
inherit NatCase;
signature pred : Self -> Self;
property pred_zero : pred(zero) = zero;
property pred_succ : all n : Self, pred(succ(n)) = n;
end;;
species NatPlus =
inherit NatDecl;
inherit NatCase;
signature plus : Self -> Self -> Self;
property zero_plus : all n : Self, plus(zero, n) = n;
property succ_plus : all m n : Self, plus(succ(m), n) = succ(plus(m, n));
......@@ -116,3 +143,5 @@ species NatPrime =
prime(p)
proof = by definition of prime;
end;;
(* even, odd, factorial, pred, iter, pow, div, mod, bit0, bit1, distance, egcd, log, gcd, lcm, chineseRemainder *)
include ../../../.config_vars
include ../../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../../logic -I ../definitions
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled .depend
include ../../../.config_vars
include ../../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../../logic -I ../definitions
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled .depend
include ../../../.config_vars
include ../../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../../logic -I ../definitions -I ../morphisms -I ../theorems
FOCALIZEC_OPT += -zvtovopt "-zenon 'zenon_transfer'" -no-coq-code
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend $(FCL_FILES:.fcl=.sk)
......@@ -11,7 +11,7 @@ HolNaturals.art: $(ART_FILES)
cat $^ > $@
HolNaturals.dk: HolNaturals.art
INCLUDE_DIRS= -I ../../core/logic -I ../../core/arith -I ../logic
INCLUDE_DIRS= -I ../../core/logic -I ../../core/arith/definitions -I ../../core/arith/morphisms -I ../logic
%.dk: %.vo
( echo "Require Coqine.";\
......
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