We've sometimes used this style in which we check the top-level constructor and then dispatch to some other function. We do not care at all about the arguments of the constructor, but we need to get the amount exactly right.
let rec st_typing_freevars
(#g:_) (#t:_) (#c:_)
(d:st_typing g t c)
: Lemma
(ensures freevars_st t `Set.subset` vars_of_env g /\
freevars_comp c `Set.subset` vars_of_env g)
(decreases d)
= match d with
| T_Abs _ _ _ _ _ _ _ _ _ -> st_typing_freevars_abs d st_typing_freevars
| T_STApp _ _ _ _ _ _ _ _
| T_STGhostApp _ _ _ _ _ _ _ _ _ _ -> st_typing_freevars_stapp d st_typing_freevars
| T_Return _ _ _ _ _ _ _ _ _ _ _ -> st_typing_freevars_return d st_typing_freevars
(* .. many more .. *)
If we had used record payloads (~and we allowed empty record patterns! to fix as well?~ #3321), we can just do | Ctor {} -> which is pretty good. Could we also do that for non-record payloads, and just expand to any amount of arguments? This is what Haskell does.
We've sometimes used this style in which we check the top-level constructor and then dispatch to some other function. We do not care at all about the arguments of the constructor, but we need to get the amount exactly right.
If we had used record payloads (~and we allowed empty record patterns! to fix as well?~ #3321), we can just do
| Ctor {} ->which is pretty good. Could we also do that for non-record payloads, and just expand to any amount of arguments? This is what Haskell does.