Irvin
Irvin
Do we still know if a tuple is allocated or it's optimized away?
Can a easy solution be to just ignore locals when in interactive mode since export_theory doesn't work now?
Lablang should also try to easily support switch statements
Here is a small example. ``` Theorem test: (!a c. A ==> B a c) ==> (!c. B a c) /\ C /\ D Proof ``` works ``` DISCH_TAC CONJ_TAC...
Another pattern to consider. `(A ==> B) ==> ~A` ~= `(A ==>B) ==> (A ==> F)`
How much of this is already existing in src/1/BoolExtractShared.sml?
Note that this was discovered using LET_ELIM_TAC. I've also encounter other weird issues due to its rewrite based implementation that perhaps there should be a non rewrite based LET_ELIM_TAC
Before REABBREV_TAC i can prove `GOO BAR = FOO BAR` after that i can't. I'm currently using the abbreviation to prevent var_eq_tac from exploding the goal
I don't know whether this theorem is good considering the v2n uses + while this one uses ||
The issue is the conflicting rewrites between ``` (v2w [] = 0w) /\ (v2w (x :: xs) = (if x then ((1w