small medium large xlarge

Back to: All Forums  PragPub
04 Apr 2013, 12:31
paul callaghan (14 posts)


The final proof needs one more step. So instead of

Main.case_one_proof = proof { intro l; intro H; rewrite (sym H); trivial; }

You need this

Main.case_one_proof = proof { intro l; intro H; compute; rewrite (sym H); trivial; }

The extra “compute” is needed because Idris doesn’t (at present) simplify the goal before trying a rewrite step. (I’m used to proof assistants which do…)

Sorry about that!

You can see more discussion on this point at

06 Sep 2017, 16:00
niusamip (1 post)

I have the same problem, hope someone will help here

You must be logged in to comment