5434 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Edwin Brady	554c395217	Made a start on the high level language	2011-10-04 14:51:00 +01:00
Edwin Brady	ff5f76217d	Rename Core to TT	2011-10-03 14:43:56 +01:00
Edwin Brady	0ae24f1b5b	Shift core TT into a separate directory (for ease of reuse)	2011-10-03 14:39:22 +01:00
Edwin Brady	ac25f15f9b	Changed contexts to Data.Map	2011-10-03 09:57:06 +01:00
Edwin Brady	575b043dea	Make sure apply doesn't solve holes automatically that the user wants to solve themselves	2011-10-03 00:24:15 +01:00
Edwin Brady	3501adbbcc	Changed way of building pattern match terms	2011-10-02 23:37:30 +01:00
Edwin Brady	c966457977	Just use proof state as TState	2011-10-01 19:44:46 +01:00
Edwin Brady	edfe9c688f	Added pattern arguments; bug fixes	2011-09-29 10:06:08 +01:00
Edwin Brady	ee3dbaa794	Change tactic names: fill for unify_fill and exact for fill	2011-09-28 22:55:02 +01:00
Edwin Brady	5dadd081d7	QED now rechecks the term, instead of just finalise. *bites fingernails*	2011-09-28 22:46:37 +01:00
Edwin Brady	44d62c7ec0	Better if unification substitutes rather than let binds	2011-09-28 22:20:17 +01:00
Edwin Brady	89ffe9bead	Undo tactic	2011-09-28 18:39:40 +01:00
Edwin Brady	ffd5e7291c	arg tactic; unification tweak	2011-09-28 14:34:12 +01:00
Edwin Brady	07f3b19571	Add patvar tactic; fix apply to deal with names properly	2011-09-28 13:29:17 +01:00
Edwin Brady	12f9368406	apply and prepare_apply elaborations	2011-09-28 13:07:25 +01:00
Edwin Brady	546e9f5b14	A gadget or two	2011-09-27 19:18:29 +01:00
Edwin Brady	5ee33765bf	make Elab a state monad for ease of EDSL programming	2011-09-27 19:07:13 +01:00
Edwin Brady	cc0dc0925d	Added elaborate; a language for composing primitive tactics.	2011-09-27 17:50:23 +01:00
Edwin Brady	cbc60eb3c5	Unification, and unify tactic	2011-09-27 14:13:32 +01:00
Edwin Brady	77be0d0042	Simple parser for data types	2011-09-26 20:03:07 +01:00
Edwin Brady	6a6a048f06	No mucking about with de Bruijn indices in proof construction	2011-09-26 12:11:41 +01:00
Edwin Brady	1921eac03b	Some tidying; compute; print	2011-09-24 22:30:03 +01:00
Edwin Brady	9c6ea4a893	Fixing evaluator bugs	2011-09-24 22:08:50 +01:00
Edwin Brady	4c68b68f8c	EvalIn and CheckIn tactics	2011-09-24 17:28:37 +01:00
Edwin Brady	d6150213e6	Purge HTT, fix evaluator and contexts	2011-09-24 14:38:50 +01:00
Edwin Brady	867f0928cb	Changed evaluator	2011-09-24 14:11:00 +01:00
Edwin Brady	56309a5de5	Minor parser changes	2011-09-23 02:11:29 +01:00
Edwin Brady	bb6bba29b4	Tactics can now complete basic proofs	2011-09-23 01:56:53 +01:00
Edwin Brady	6923ac18b5	Started theorem prover and tactics	2011-09-22 00:22:19 +01:00
Edwin Brady	ccd64c758f	Beginning of proof shell	2011-09-21 23:13:45 +01:00
Edwin Brady	205fcef434	Some proof state, some showing of terms	2011-09-21 17:16:07 +01:00
Edwin Brady	f35b3f09f3	Fix LICENSE	2011-09-14 18:01:24 +01:00
Edwin Brady	dc0c198f0c	First lot of source files and paper	2011-09-14 17:59:07 +01:00
Edwin Brady	6aac1a90a5	First commit	2011-09-14 17:56:36 +01:00