case ty_0 of {
LamAbs x t t0 ->
case decOpt (decOptappears_bound_in_tm x t0) init_size of {
For every binder, it checks if that name appears bound in the subterm. This is a result of how QuickChick generates the decision procedure from the inductive specification (which mentions appears_bound_in).
This can be linear, if we have access to the set of bound variables in the sub-term, which can be computed bottom-up in the same traversal as the decision procedure. Unclear if quickchick will support this. The alternative is to do a handwritten decision procedure.
From the extracted Haskell code:
For every binder, it checks if that name appears bound in the subterm. This is a result of how QuickChick generates the decision procedure from the inductive specification (which mentions
appears_bound_in).This can be linear, if we have access to the set of bound variables in the sub-term, which can be computed bottom-up in the same traversal as the decision procedure. Unclear if quickchick will support this. The alternative is to do a handwritten decision procedure.