https://github.com/EasyCrypt/easycrypt
Revision 65eda54a29631522fa7bf37c8c68ceb3629c1d50 authored by Pierre-Yves Strub on 01 December 2015, 17:10:55 UTC, committed by Pierre-Yves Strub on 01 December 2015, 17:10:55 UTC
Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much.
1 parent e6a3241
Tip revision: 65eda54a29631522fa7bf37c8c68ceb3629c1d50 authored by Pierre-Yves Strub on 01 December 2015, 17:10:55 UTC
Hint database for auto-exact.
Hint database for auto-exact.
Tip revision: 65eda54
Makefile.system
# -*- Makefile -*-
# --------------------------------------------------------------------
OCAML := $(shell ocamlbuild -which ocamlc 2>/dev/null || echo false)
CC := gcc
MACHINE := $(shell $(OCAML) -ccopt -dumpmachine dummy.c 2>/dev/null)
UNAME := $(shell uname -s)
EXE :=
ifneq (,$(findstring CYGWIN,$(UNAME)))
CC = $(MACHINE)-gcc
endif
ifneq (,$(findstring mingw,$(MACHINE)))
EXE := .exe
endif
ifneq (,$(findstring cygwin,$(MACHINE)))
EXE := .exe
endif
Computing file changes ...
