Module Hints.Induct
type t
=
|
Functional of
{
f_name : string;
}
functional induction
|
Structural of
{
style : [ `Multiplicative | `Additive ];
vars : string list;
}
structural induction
|
Default
val default : t
val print : t CCFormat.printer
val chash : t Imandra_util.Chash.hasher