Tips and tricks for writing functions that take proofs as arguments.
Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (
UntypedAST) and one for typed terms (
TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!
You write a few programs…
Example well_typed := UAdd (UNat 1) (UNat 1). Example ill_typed := UAdd (UNat 1) (UBool true).
… typecheck them:
Definition tc_good := typecheck well_typed.Definition tc_bad := typecheck ill_typed.
… and attempt to run them:
interp takes a
typecheck returns an
option. What do we do?