let lt e1 e2 = CompProp e1 C_Lt e2
let lt e1 e2 =
CompProp e1 C_Lt e2
FStar.Reflection.V2.Arith.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
FStar.Reflection.V2.Arith.fst
FStar.Reflection.V2.Arith.expr FStar.Reflection.V2.Arith.CompProp FStar.Reflection.V2.Arith.C_Lt FStar.Reflection.V2.Arith.prop
(*
   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.Reflection.V2.Arith

open FStar.Tactics.V2
open FStar.Reflection.V2
module O = FStar.Order

(*
 * Simple decision procedure to decide if a term is an "arithmetic
 * proposition", by which we mean a simple relation between two
 * arithmetic expressions (each representing integers or naturals)
 *
 * Main use case: deciding, in a tactic, if a goal is an arithmetic
 * expression and applying a custom decision procedure there (instead of
 * feeding to the SMT solver)
 *)

noeq
type expr =
    | Lit     : int -> expr
    // atom, contains both a numerical ID and the actual term encountered
    | Atom    : nat -> term -> expr
    | Plus    : expr -> expr -> expr
    | Mult    : expr -> expr -> expr
    | Minus   : expr -> expr -> expr
    | Land    : expr -> expr -> expr
    | Lxor    : expr -> expr -> expr
    | Lor     : expr -> expr -> expr
    | Ladd    : expr -> expr -> expr
    | Lsub    : expr -> expr -> expr
    | Shl     : expr -> expr -> expr
    | Shr     : expr -> expr -> expr
    | Neg     : expr -> expr
    | Udiv    : expr -> expr -> expr
    | Umod    : expr -> expr -> expr
    | MulMod  : expr -> expr -> expr
    | NatToBv : expr -> expr
    // | Div   : expr -> expr -> expr // Add this one?

noeq
type connective =
    | C_Lt | C_Eq | C_Gt | C_Ne

noeq
type prop =
    | CompProp : expr -> connective -> expr -> prop
    | AndProp  : prop -> prop -> prop
    | OrProp   : prop -> prop -> prop
    | NotProp  : prop -> prop
val lt : e1: FStar.Reflection.V2.Arith.expr -> e2: FStar.Reflection.V2.Arith.expr
  -> FStar.Reflection.V2.Arith.prop
e1: FStar.Reflection.V2.Arith.expr -> e2: FStar.Reflection.V2.Arith.expr
  -> FStar.Reflection.V2.Arith.prop