val empty_decreaser (#a: Type u#a) (x: a) : Tot (acc_classical (empty_relation #a) x) (decreases x)
let rec empty_decreaser (#a: Type u#a) (x: a)
  : Tot (acc_classical (empty_relation #a) x) (decreases x) =
  let smaller (y: a{empty_relation y x}) : acc_classical (empty_relation #a) y =
    empty_decreaser y
  in
  AccClassicalIntro smaller
val empty_decreaser (#a: Type u#a) (x: a) : Tot (acc_classical (empty_relation #a) x) (decreases x)
let rec empty_decreaser (#a: Type u#a) (x: a)
    : Tot (acc_classical (empty_relation #a) x) (decreases x) =
let smaller (y: a{empty_relation y x}) : acc_classical (empty_relation #a) y = empty_decreaser y in
AccClassicalIntro smaller
FStar.WellFoundedRelation.fst.checked
prims.fst.checked FStar.WellFounded.Util.fsti.checked FStar.WellFounded.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked
FStar.WellFoundedRelation.fst
FStar.WellFoundedRelation.AccClassicalIntro FStar.WellFoundedRelation.empty_relation FStar.WellFoundedRelation.acc_classical FStar.WellFoundedRelation.empty_decreaser
(*
   Copyright 2022 Jay Lorch and Nikhil Swamy, 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.
*)

(* This library is intended to simplify using well-founded relations
   in decreases clauses.
*)

module FStar.WellFoundedRelation

open FStar.Universe
module WF = FStar.WellFounded
module WFU = FStar.WellFounded.Util

let rec default_decreaser (#a: Type u#a) (x: a)
  : Tot (acc_classical (default_relation #a) x) (decreases x) =
  let smaller (y: a{default_relation y x}) : acc_classical (default_relation #a) y =
    default_decreaser y
  in
  AccClassicalIntro smaller

let default_wfr (a: Type u#a) : (wfr: wfr_t a{wfr.relation == default_relation}) =
  let proof (x1: a) (x2: a)
    : Lemma (requires default_relation x1 x2)
            (ensures default_decreaser x1 << default_decreaser x2) =
    assert ((default_decreaser x2).access_smaller x1 == default_decreaser x1)
  in
  { relation = default_relation; decreaser = default_decreaser; proof = proof; }
val empty_decreaser (#a: Type u#a) (x: a) : Tot (acc_classical (empty_relation #a) x) (decreases x)
x: a
  -> Prims.Tot (FStar.WellFoundedRelation.acc_classical FStar.WellFoundedRelation.empty_relation x)