Skip to main content

Browse the archive

Revision 2afb775be1173eb4ff8aae7993277d0652575273 authored by Pierre-Yves Strub on 14 April 2021, 15:27:25 UTC, committed by Pierre-Yves Strub on 14 April 2021, 15:27:25 UTC 
StdLib: funi + same weight => eq
1 parent 5df6a6f
Raw File
ecCallbyValue.mli 
(* -------------------------------------------------------------------- *)
open EcFol
open EcEnv
open EcReduction

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