val equational (t: term) : bool
let equational (t:term) : bool =
  match t.t with
  | Tm_FStar host_term ->
    (match R.inspect_ln host_term with
     | R.Tv_Match _ _ _ -> true
     | _ -> false)
  | _ -> false
val equational (t: term) : bool
let equational (t: term) : bool =
match t.t with
| Tm_FStar host_term ->
  (match R.inspect_ln host_term with
    | R.Tv_Match _ _ _ -> true
    | _ -> false)
| _ -> false
Pulse.Checker.Prover.Match.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Prover.Util.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Prover.Match.fst
Pulse.Syntax.Base.term Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.host_term FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.term FStar.Pervasives.Native.option FStar.Reflection.Types.match_returns_ascription Prims.list FStar.Reflection.V2.Data.branch FStar.Reflection.V2.Data.term_view Prims.bool Pulse.Syntax.Base.term'
module Pulse.Checker.Prover.Match

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Typing.Metatheory
open Pulse.Typing.Util
open Pulse.Checker.VPropEquiv
open Pulse.Checker.Prover.Base
open Pulse.Checker.Prover.Util

module L = FStar.List.Tot
module R = FStar.Reflection.V2
module TermEq = FStar.Reflection.V2.TermEq
module T = FStar.Tactics.V2

module RUtil = Pulse.Reflection.Util
module P = Pulse.Syntax.Printer
module PS = Pulse.Checker.Prover.Substs
val equational (t: term) : bool
t: Pulse.Syntax.Base.term -> Prims.bool