fstar 2022.01.15 · OCaml Package

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

val step : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val step_lemma : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val canon_point : 
  FStar_Reflection_Arith.expr ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Arith.expr FStar_Tactics_Result.__result

val canon_point_entry : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val canon : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result