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

module N = FStar_TypeChecker_Normalize

module E = FStar_Tactics_Effect

module B = FStar_Tactics_Basic

module TM = FStar_Tactics_Monad

module CTRW = FStar_Tactics_CtrlRewrite

module RT = FStar_Reflection_Types

module RD = FStar_Reflection_Data

module EMB = FStar_Syntax_Embeddings

module NBET = FStar_TypeChecker_NBETerm

val interpret_tac : 
  'a TM.tac ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val uninterpret_tac : 
  'a FStar_Tactics_Effect.__tac ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val tr1 : FStar_Pervasives.norm_step -> EMB.norm_step

val rt1 : EMB.norm_step -> FStar_Pervasives.norm_step

val e_norm_step' : FStar_Pervasives.norm_step EMB.embedding

val e_norm_step_nbe' : FStar_Pervasives.norm_step NBET.embedding

val tr_repr_steps : FStar_Pervasives.norm_step list -> EMB.norm_step list

val to_tac_0 : 'a FStar_Tactics_Effect.__tac -> 'a TM.tac

val to_tac_1 : ('b -> 'a FStar_Tactics_Effect.__tac) -> 'b -> 'a TM.tac

val from_tac_1 : ('a -> 'b TM.tac) -> 'a -> 'b FStar_Tactics_Effect.__tac

val from_tac_2 : 
  ('a -> 'b -> 'c TM.tac) ->
  'a ->
  'b ->
  'c FStar_Tactics_Effect.__tac

val from_tac_3 : 
  ('a -> 'b -> 'c -> 'd TM.tac) ->
  'a ->
  'b ->
  'c ->
  'd FStar_Tactics_Effect.__tac

val set_goals : 
  FStar_Tactics_Types.goal Prims.list ->
  Prims.unit FStar_Tactics_Effect.__tac

val set_smt_goals : 
  FStar_Tactics_Types.goal Prims.list ->
  Prims.unit FStar_Tactics_Effect.__tac

val top_env : Prims.unit -> B.env FStar_Tactics_Effect.__tac

val fresh : Prims.unit -> FStar_BigInt.t FStar_Tactics_Effect.__tac

val refine_intro : Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac

val tc : 
  B.env ->
  FStar_Syntax_Syntax.term ->
  FStar_Reflection_Data.typ FStar_Tactics_Effect.__tac

val tcc : 
  B.env ->
  FStar_Syntax_Syntax.term ->
  FStar_Syntax_Syntax.comp FStar_Tactics_Effect.__tac

val unshelve : 
  FStar_Syntax_Syntax.term ->
  Prims.unit FStar_Tactics_Effect.__tac

val unquote : 'a -> 'b

val norm : 
  FStar_Pervasives.norm_step list ->
  Prims.unit FStar_Tactics_Effect.__tac

val norm_term_env : 
  B.env ->
  FStar_Pervasives.norm_step list ->
  FStar_Syntax_Syntax.term ->
  FStar_Syntax_Syntax.term FStar_Tactics_Effect.__tac

val norm_binder_type : 
  FStar_Pervasives.norm_step list ->
  FStar_Syntax_Syntax.binder ->
  Prims.unit FStar_Tactics_Effect.__tac

val intro : Prims.unit -> FStar_Syntax_Syntax.binder FStar_Tactics_Effect.__tac

val intro_rec : 
  Prims.unit ->
  (FStar_Syntax_Syntax.binder * FStar_Syntax_Syntax.binder)
    FStar_Tactics_Effect.__tac

val rename_to : 
  FStar_Syntax_Syntax.binder ->
  Prims.string ->
  FStar_Syntax_Syntax.binder FStar_Tactics_Effect.__tac

val revert : Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac

val binder_retype : 
  FStar_Syntax_Syntax.binder ->
  Prims.unit FStar_Tactics_Effect.__tac

val clear_top : Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac

val clear : FStar_Syntax_Syntax.binder -> Prims.unit FStar_Tactics_Effect.__tac

val rewrite : 
  FStar_Syntax_Syntax.binder ->
  Prims.unit FStar_Tactics_Effect.__tac

val t_exact : 
  Prims.bool ->
  Prims.bool ->
  FStar_Syntax_Syntax.term ->
  Prims.unit FStar_Tactics_Effect.__tac

val t_apply : 
  Prims.bool ->
  Prims.bool ->
  FStar_Syntax_Syntax.term ->
  Prims.unit FStar_Tactics_Effect.__tac

val t_apply_lemma : 
  Prims.bool ->
  Prims.bool ->
  FStar_Syntax_Syntax.term ->
  Prims.unit FStar_Tactics_Effect.__tac

val print : Prims.string -> Prims.unit FStar_Tactics_Effect.__tac

val debugging : Prims.unit -> Prims.bool FStar_Tactics_Effect.__tac

val dump : Prims.string -> Prims.unit FStar_Tactics_Effect.__tac

val dump_all : 
  Prims.bool ->
  Prims.string ->
  Prims.unit FStar_Tactics_Effect.__tac

val dump_uvars_of : 
  FStar_Tactics_Types.goal ->
  Prims.string ->
  Prims.unit FStar_Tactics_Effect.__tac

val t_trefl : Prims.bool -> Prims.unit FStar_Tactics_Effect.__tac

val dup : Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac

val prune : Prims.string -> Prims.unit FStar_Tactics_Effect.__tac

val addns : Prims.string -> Prims.unit FStar_Tactics_Effect.__tac

val t_destruct : 
  FStar_Syntax_Syntax.term ->
  (FStar_Syntax_Syntax.fv * FStar_BigInt.t) Prims.list
    FStar_Tactics_Effect.__tac

val set_options : Prims.string -> Prims.unit FStar_Tactics_Effect.__tac

val uvar_env : 
  B.env ->
  FStar_Reflection_Data.typ FStar_Pervasives_Native.option ->
  FStar_Syntax_Syntax.term FStar_Tactics_Effect.__tac

val unify_env : 
  B.env ->
  FStar_Syntax_Syntax.term ->
  FStar_Syntax_Syntax.term ->
  Prims.bool FStar_Tactics_Effect.__tac

val unify_guard_env : 
  B.env ->
  FStar_Syntax_Syntax.term ->
  FStar_Syntax_Syntax.term ->
  Prims.bool FStar_Tactics_Effect.__tac

val match_env : 
  B.env ->
  FStar_Syntax_Syntax.term ->
  FStar_Syntax_Syntax.term ->
  Prims.bool FStar_Tactics_Effect.__tac

val launch_process : 
  Prims.string ->
  Prims.string Prims.list ->
  Prims.string ->
  Prims.string FStar_Tactics_Effect.__tac

val fresh_bv_named : 
  Prims.string ->
  FStar_Reflection_Data.typ ->
  FStar_Syntax_Syntax.bv FStar_Tactics_Effect.__tac

val change : FStar_Reflection_Data.typ -> Prims.unit FStar_Tactics_Effect.__tac

val get_guard_policy : 
  Prims.unit ->
  FStar_Tactics_Types.guard_policy FStar_Tactics_Effect.__tac

val set_guard_policy : 
  FStar_Tactics_Types.guard_policy ->
  Prims.unit FStar_Tactics_Effect.__tac

val lax_on : Prims.unit -> Prims.bool FStar_Tactics_Effect.__tac

val tadmit_t : 
  FStar_Syntax_Syntax.term ->
  Prims.unit FStar_Tactics_Effect.__tac

val join : Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac

val inspect : 
  FStar_Syntax_Syntax.term ->
  FStar_Reflection_Data.term_view FStar_Tactics_Effect.__tac

val pack : 
  FStar_Reflection_Data.term_view ->
  FStar_Syntax_Syntax.term FStar_Tactics_Effect.__tac

val curms : Prims.unit -> FStar_BigInt.t FStar_Tactics_Effect.__tac

val set_urgency : FStar_BigInt.t -> Prims.unit FStar_Tactics_Effect.__tac

val t_commute_applied_match : 
  Prims.unit ->
  Prims.unit FStar_Tactics_Effect.__tac

val fix_either : 
  ('a, 'b) FStar_Pervasives.either ->
  ('a, 'b) FStar_Pervasives.either

val fmap : 
  ('a -> 'b) ->
  'a FStar_Tactics_Result.__result ->
  'b FStar_Tactics_Result.__result

val catch : 
  (Prims.unit -> 'a FStar_Tactics_Effect.__tac) ->
  (Prims.exn, 'a) FStar_Pervasives.either FStar_Tactics_Effect.__tac

val recover : 
  (Prims.unit -> 'a FStar_Tactics_Effect.__tac) ->
  (Prims.exn, 'a) FStar_Pervasives.either FStar_Tactics_Effect.__tac

val ctrl_rewrite : 
  FStar_Tactics_Types.direction ->
  (RT.term ->
    (Prims.bool * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Effect.__tac) ->
  (Prims.unit -> Prims.unit FStar_Tactics_Effect.__tac) ->
  Prims.unit FStar_Tactics_Effect.__tac