Skip to main content

Browse the archive

Revision cdc065eecfa65fc3613cd21ec0882f9209700b02 authored by Christian Doczkal on 11 May 2022, 08:47:50 UTC, committed by Pierre-Yves Strub on 12 May 2022, 06:43:29 UTC 
[stdlib]: add various small lemmas (Logic, FSet, Distr, DInterval, Bigop)
 
- #non-backward-compatible: this commits generalizes `Bigop.reindex`
  to restrict the cancellation property to the index list.
1 parent de42d06
Raw File
ecCallbyValue.mli 
(* -------------------------------------------------------------------- *)
open EcFol
open EcEnv
open EcReduction

(* -------------------------------------------------------------------- *)
val norm_cbv : reduction_info -> LDecl.hyps -> form -> form
back to top