Hey all! I was practicing verifying lemmas in F* from the tutorial, and I came across a few things that I didn't really understand.
From https://www.fstar-lang.org/tutorial/tutorial.html#sec-to-type-intrinsically-or-to-prove-lemmas : ''' val reverse: #a:Type -> f:(list a -> Tot (list a)){forall l. l == f (f l) However, F* refuses to accept this as a valid type for reverse: proving this property requires two separate inductions, neither of which F* can perform automatically. ''' Why can't F* perform these inductions automatically? What are the bounds of inference on the SMT solver? Can someone shoot me resources on the same? Sincerely, Nitin John Raj
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
