Zulip Chat Archive
Stream: general
Topic: normal form in tactics mode
petercommand (Dec 01 2018 at 14:31):
is there any tactic that can be used to reduce a type to head normal form in tactics mode? thanks!
petercommand (Dec 01 2018 at 14:32):
like coq's compute tactic
Mario Carneiro (Dec 01 2018 at 14:38):
whnf
petercommand (Dec 01 2018 at 14:51):
hmm, I have no idea how to use whnf..
petercommand (Dec 01 2018 at 14:51):
I want to reduce the goal to hnf though, not whnf
Last updated: Dec 20 2023 at 11:08 UTC