Skip to content

Instantly share code, notes, and snippets.

@sellout

sellout/gist:799d08c58ce5610a6fcc

Created May 2, 2014 17:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sellout/799d08c58ce5610a6fcc to your computer and use it in GitHub Desktop.
Save sellout/799d08c58ce5610a6fcc to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.idr
ihe__2 : progDenote (compile e__2 ++ p) s = progDenote p (expDenote e__2 :: s)
---------- Goal: ----------
{hole12} : progDenote (compile e__2 ++ (compile e__0 ++ [iBinop b__0]) ++ p) s = progDenote p (binopDenote b__0 (expDenote e__0) (expDenote e__2) :: s)
-- when I try
rewrite ihe__2
-- nothing happens … how do I get it to rewrite the goal into
{hole12} : progDenote ((compile e__0 ++ [iBinop b__0]) ++ p) (expDenote e__2 :: s) = progDenote p (binopDenote b__0 (expDenote e__0) (expDenote e__2) :: s)
-- ?
@sellout
Copy link
Author

sellout commented May 2, 2014

The proof so far:

-- intro
-- induction e
-- intros
-- compute
-- refine refl
-- intros
-- compute
-- rewrite appendAssociative (compile e__2) (compile e__0 ++ [iBinop b__0]) p

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment