Irvin

Results 47 comments of Irvin

Implement parser that supports unsupported features

`open` `infix`

Efficient peep-hole optimisation for DataLang

Is there any reason a simple forward propagation can't be done? The effects of this peephole optimization in the example given seems to be similar to PolyML simplification pass. As...

Tactictoe selftests seem to fail.

https://github.com/HOL-Theorem-Prover/HOL/issues/1541 is probably the cause of this breakage

Try to store only delta's in translator Part 1

DO NOT MERGE. I'm only opening a PR to test with regression

Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

I've figured out why this is way slower than using MP with a induction thm + GENL. https://github.com/HOL-Theorem-Prover/HOL/blob/a902f2db73f6a761d57905ec18eb06291ad8a9b9/src/1/Thm_cont.sml#L104-L133 This bug fix means that the thm passed through the continuation gets...

Better simplification of preconditions for eq_lemmas

the full list if anyone's interested [⊢ IsTypeRep AST_EXP_v AST_EXP_TYPE ∧ IsTypeRep (LIST_v (PAIR_v HOL_STRING_v (PAIR_v HOL_STRING_v AST_EXP_v))) (LIST_TYPE (PAIR_TYPE HOL_STRING_TYPE (PAIR_TYPE HOL_STRING_TYPE AST_EXP_TYPE))) ∧ IsTypeRep AST_PAT_v AST_PAT_TYPE ⇒ IsTypeRep...

Clean up dataLang cost semantics

```quote The `allowed_op` definition serves no purpose anymore --- all operators except Install are now allowed, and Install is already treated specially elsewhere in `do_app` ``` This the only actual...