val maybe_intros: Prims.unit -> Tac unit
let rec maybe_intros () : Tac unit =
  let g = cur_goal () in
  match inspect_ln g with
  | Reflection.V2.Tv_Arrow _ _ ->
    ignore (intro ());
    maybe_intros ()
  | _ -> ()
val maybe_intros: Prims.unit -> Tac unit
let rec maybe_intros () : Tac unit =
let g = cur_goal () in
match inspect_ln g with
| Reflection.V2.Tv_Arrow _ _ ->
  ignore (intro ());
  maybe_intros ()
| _ -> ()
FStar.Tactics.Typeclasses.fst.checked
prims.fst.checked FStar.Tactics.V2.SyntaxHelpers.fst.checked FStar.Tactics.V2.SyntaxCoercions.fst.checked FStar.Tactics.V2.Derived.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Util.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.Common.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Tactics.Typeclasses.fst
Prims.unit FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.binder FStar.Reflection.Types.comp FStar.Tactics.Typeclasses.maybe_intros FStar.Pervasives.ignore FStar.Reflection.V2.Data.binding FStar.Tactics.V2.Builtins.intro FStar.Reflection.V2.Data.term_view FStar.Reflection.Types.typ FStar.Tactics.V2.Derived.cur_goal
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Tactics.Typeclasses

open FStar.Reflection.V2
open FStar.Tactics.Common
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.V2.SyntaxHelpers
open FStar.Tactics.V2.Derived
open FStar.Tactics.V2.SyntaxCoercions
open FStar.Tactics.NamedView

module L = FStar.List.Tot.Base
let (@) = L.op_At

(* The attribute that marks classes *)
irreducible
let tcclass : unit = ()

(* The attribute that marks instances *)
irreducible
let tcinstance : unit = ()

(* The attribute that marks class fields
   to signal that no method should be generated for them *)
irreducible
let no_method : unit = ()

private
let rec first (f : 'a -> Tac 'b) (l : list 'a) : Tac 'b =
    match l with
    | [] -> fail "no cands"
    | x::xs -> (fun () -> f x) `or_else` (fun () -> first f xs)

(* TODO: memoization?. And better errors. *)
private
let rec tcresolve' (seen:list term) (fuel:int) : Tac unit =
    if fuel <= 0 then
        fail "out of fuel";
    debug ("fuel = " ^ string_of_int fuel);
    let g = cur_goal () in
    if L.existsb (term_eq g) seen then
      fail "loop";
    let seen = g :: seen in
    local seen fuel `or_else` (fun () -> global seen fuel `or_else` (fun () -> fail ("could not solve constraint: " ^ term_to_string g)))
and local (seen:list term) (fuel:int) () : Tac unit =
    let bs = vars_of_env (cur_env ()) in
    first (fun (b:binding) -> trywith seen fuel (pack (Tv_Var b))) bs
and global (seen:list term) (fuel:int) () : Tac unit =
    let cands = lookup_attr (`tcinstance) (cur_env ()) in
    first (fun fv -> trywith seen fuel (pack (Tv_FVar fv))) cands
and trywith (seen:list term) (fuel:int) (t:term) : Tac unit =
    debug ("Trying to apply hypothesis/instance: " ^ term_to_string t);
    (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen (fuel-1))
val maybe_intros: Prims.unit -> Tac unit
_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit