swh:1:snp:04e159a4411e97cbe416dcf21d082639f654120b
- HEAD
- refs/heads/1.0
- refs/heads/1.0-preview
- refs/heads/aprhl
- refs/heads/csidh-group-action
- refs/heads/deploy-assign
- refs/heads/deploy-better-dlet
- refs/heads/deploy-better-int-red
- refs/heads/deploy-better-printing
- refs/heads/deploy-bigop-split
- refs/heads/deploy-binomial-law
- refs/heads/deploy-cdh-rsr
- refs/heads/deploy-chachapoly
- refs/heads/deploy-chernoff
- refs/heads/deploy-clean-oldmonoid
- refs/heads/deploy-clean-pow
- refs/heads/deploy-codepos-fix
- refs/heads/deploy-cost
- refs/heads/deploy-cost-1.0-preview
- refs/heads/deploy-cost-submitted
- refs/heads/deploy-crt
- refs/heads/deploy-cyclic
- refs/heads/deploy-debug-mark
- refs/heads/deploy-derandomize
- refs/heads/deploy-dexcepted-sampling
- refs/heads/deploy-djoin-dlist
- refs/heads/deploy-eager-rp
- refs/heads/deploy-eco2
- refs/heads/deploy-eqv-quotient
- refs/heads/deploy-expected-cost
- refs/heads/deploy-extended-tests
- refs/heads/deploy-fingroup
- refs/heads/deploy-fix-17390
- refs/heads/deploy-fmatch
- refs/heads/deploy-for
- refs/heads/deploy-general-prf-distinguisher
- refs/heads/deploy-global-union
- refs/heads/deploy-implicit-arguments
- refs/heads/deploy-improve-matching
- refs/heads/deploy-instance-adv
- refs/heads/deploy-lamport
- refs/heads/deploy-map-find
- refs/heads/deploy-match
- refs/heads/deploy-match-in-stmt
- refs/heads/deploy-match-in=prog-logic-houra
- refs/heads/deploy-mathml
- refs/heads/deploy-mem-in-types
- refs/heads/deploy-minr-maxr
- refs/heads/deploy-momemtum
- refs/heads/deploy-new-cost
- refs/heads/deploy-new-rom
- refs/heads/deploy-no-eco
- refs/heads/deploy-nosmt-ops
- refs/heads/deploy-oaep
- refs/heads/deploy-opaque-op
- refs/heads/deploy-oracle-pke
- refs/heads/deploy-poly-record
- refs/heads/deploy-polymorphic-module
- refs/heads/deploy-ppe-with-full-path
- refs/heads/deploy-prod-fintype
- refs/heads/deploy-quantum
- refs/heads/deploy-reduce-decimal
- refs/heads/deploy-reduction
- refs/heads/deploy-remove-cut
- refs/heads/deploy-rewrite-patterns
- refs/heads/deploy-rigid-auto-rewrite
- refs/heads/deploy-rigid-opt
- refs/heads/deploy-ring-ideal
- refs/heads/deploy-rom-nobranching
- refs/heads/deploy-search
- refs/heads/deploy-section
- refs/heads/deploy-sem
- refs/heads/deploy-sigmaprotocols
- refs/heads/deploy-simpler-rp
- refs/heads/deploy-simpler-xpaths
- refs/heads/deploy-solveeq
- refs/heads/deploy-subst-crush
- refs/heads/deploy-tactic-in-rewrite
- refs/heads/deploy-taylor
- refs/heads/deploy-tc
- refs/heads/deploy-test-script
- refs/heads/deploy-theory-matrix
- refs/heads/deploy-theory-matrix-ring
- refs/heads/deploy-theory-monalg
- refs/heads/deploy-theory-symmetric-group
- refs/heads/deploy-tighter-birthday
- refs/heads/deploy-transeq
- refs/heads/deploy-trivial-in-low-api
- refs/heads/deploy-tutorial
- refs/heads/deploy-weak-dep-types
- refs/heads/deploy-wf
- refs/heads/deploy-why3-1.4
- refs/heads/deploy-wp-kw
- refs/heads/draft-typeclass
- refs/heads/ellora
- refs/heads/try-merge-section
- refs/heads/typeclass-draft
- refs/tags/ccs14-sfe
- refs/tags/doc
- refs/tags/evoting
Permalinks
To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used.
Select below a type of object currently browsed in order to display its associated SWHID and permalink.
Tip revision: 7c35bc466c977edb46bcc1a4fc4e069c212f2a20 authored by Alley Stoughton on 28 April 2021, 13:36:14 UTC
Simplified recursion theorem to not use predecs, but just well-founded
Simplified recursion theorem to not use predecs, but just well-founded
Tip revision: 7c35bc4
ecCallbyValue.mli
(* -------------------------------------------------------------------- *)
open EcFol
open EcEnv
open EcReduction
(* -------------------------------------------------------------------- *)
val norm_cbv : reduction_info -> LDecl.hyps -> form -> form
