fstar 2022.01.15 · OCaml Package

fstar

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

in-package search v0.1.0

package fstar

Legend:
Library
Module
Module type
Parameter
Class
Class type

type proposition = FStar_Reflection_Types.term

val proposition_to_string : proposition -> Prims.string

type assertions = {

pres : proposition Prims.list;
posts : proposition Prims.list;

}

val __proj__Mkassertions__item__pres : assertions -> proposition Prims.list

val __proj__Mkassertions__item__posts : assertions -> proposition Prims.list

val mk_assertions : 
  proposition Prims.list ->
  proposition Prims.list ->
  assertions

val simpl_norm_steps : FStar_Pervasives.norm_step Prims.list

val is_trivial_proposition : 
  proposition ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val simp_filter_proposition : 
  FStar_Reflection_Types.env ->
  FStar_Pervasives.norm_step Prims.list ->
  proposition ->
  FStar_Tactics_Types.proofstate ->
  proposition Prims.list FStar_Tactics_Result.__result

val simp_filter_propositions : 
  FStar_Reflection_Types.env ->
  FStar_Pervasives.norm_step Prims.list ->
  proposition Prims.list ->
  FStar_Tactics_Types.proofstate ->
  proposition Prims.list FStar_Tactics_Result.__result

val simp_filter_assertions : 
  FStar_Reflection_Types.env ->
  FStar_Pervasives.norm_step Prims.list ->
  assertions ->
  FStar_Tactics_Types.proofstate ->
  assertions FStar_Tactics_Result.__result