Open nskh opened 2 months ago
@Negabinary: I addressed your changes, should be ready for review. We can merge as-is, or discuss how to add in some way to invoke a stepper by adding a proof
keyword here too.
theorem name = typ
proof "serialized stepper data"
in e
things we need in the typ syntax:
forall x -> ty
exists x : T -> typ. [sigma types]
(x : typ) -> typ. [pi types]
(syntactic sugar: forall x : T -> ty)
typ(typ).
e1 = e2. [equality types]
If we do the syntax as:
theorem name : typ
proof e1
in e2
then this becomes just another let expression exactly -- that should be pretty straightforward to do so let's update this PR in that direction, then make another PR for adding the new type forms.
TODO:
theorem pat = exp in exp
, which matches let expressions exactlyforall
to type
forall pat -> ty
construct to types{e1 = e2}
form to types
Replaces https://github.com/hazelgrove/hazel/pull/1263.
In-progress PR to add a theorem keyword in the style of let-equals-in to Hazel.
Based on stepper-rewrites this time.