You also need to translate "with" as a forall (pi binder) as well. Then, you'll ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		tel on May 28, 2015 \| parent \| context \| favorite \| on: Calculus for mathematicians (1997) [pdf] You also need to translate "with" as a forall (pi binder) as well. Then, you'll merely note that the formula is unsatisfiable without demonstrating a proof that y is within the proper bounds.

eli_gottlieb on May 28, 2015 [–]

Oh good, so I'm not the only one whose mind tries to translate mathematical prose into the notation of dependent type theory!

tel on May 28, 2015 | [–]

Sometimes your problem really does just call for a hammer :)

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact