Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ringLib] RING_TAC|RULE ported from HOL-Light #1240

Merged
merged 1 commit into from
May 31, 2024
Merged

[ringLib] RING_TAC|RULE ported from HOL-Light #1240

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
20 changes: 15 additions & 5 deletions examples/algebra/ring/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,21 +1,31 @@
INCLUDES = $(HOLDIR)/src/pred_set/src/more_theories $(HOLDIR)/src/integer \
$(HOLDIR)/src/algebra/construction

ifdef POLY
all: $(DEFAULT_TARGETS) selftest.exe
.PHONY: all

HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) selftest.exe ring-selftest.log

selftest.exe: selftest.uo ringLib.uo
$(HOLMOSMLC) -o $@ $<

ifdef POLY
OBJS = pred_set/src/more_theories/cardinalTheory integer/intLib \
algebra/construction/ringTheory

FULL_OBJPATHS = $(patsubst %,$(HOLDIR)/src/%.uo,$(OBJS))

EXTRA_CLEANS = $(HOLHEAP)

all: $(HOLHEAP)

$(HOLHEAP): $(FULL_OBJPATHS) $(HOLDIR)/bin/hol.state
$(protect $(HOLDIR)/bin/buildheap) $(DEBUG_FLAG) -o $@ $(FULL_OBJPATHS)
endif

all: $(DEFAULT_TARGETS)
ifdef HOLSELFTESTLEVEL
all: ring-selftest.log

.PHONY: all
ring-selftest.log: selftest.exe
$(tee ./selftest.exe 2>&1, $@)

endif
15 changes: 15 additions & 0 deletions examples/algebra/ring/ringLib.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
(* ========================================================================= *)
(* A decision procedure for the universal theory of rings *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* (c) Copyright, University of Cambridge 1998 *)
(* ========================================================================= *)

signature ringLib =
sig

include Abbrev

val RING_RULE : term -> thm
val RING_TAC : tactic
end