An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem with the theory, but because I didn't understand how Bound works sadly.)
It would be nice to let things be either checked or inferred... When in checking mode, then _ could be put in instead of a term, and it would be inferred by unification.
Changing the syntax to have maybes in places, and then merging check and infer into one function might be the way. This seems to be the Weirich approach.
It would be nice to let things be either checked or inferred... When in checking mode, then
_could be put in instead of a term, and it would be inferred by unification.Changing the syntax to have maybes in places, and then merging
checkandinferinto one function might be the way. This seems to be the Weirich approach.