swh:1:snp:deb9fd355bffe3d96f042bd4e5113afbb0d7cbb2
- HEAD
- refs/heads/1.0
- refs/heads/1.0-preview
- refs/heads/aprhl
- refs/heads/deploy-assign
- refs/heads/deploy-better-dlet
- refs/heads/deploy-better-int-red
- refs/heads/deploy-better-printing
- refs/heads/deploy-binomial-law
- refs/heads/deploy-chachapoly
- refs/heads/deploy-chernoff
- refs/heads/deploy-clean-pow
- refs/heads/deploy-cloning-with-theories
- 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-eager-rp
- refs/heads/deploy-eco2
- refs/heads/deploy-eqv-quotient
- 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-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-rom
- refs/heads/deploy-no-eco
- refs/heads/deploy-nosmt-ops
- refs/heads/deploy-oaep
- refs/heads/deploy-opaque-op
- refs/heads/deploy-poly-record
- refs/heads/deploy-polymorphic-module
- 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-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-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/typeclass-draft
- refs/tags/ccs14-sfe
- refs/tags/doc
- refs/tags/evoting
Cook and download a directory from the Software Heritage Vault
You have requested the cooking of the directory with identifier swh:1:dir:52ec95fb47d65c214ed388293c06ccb8676ef4d6 into a standard tar.gz archive.
Are you sure you want to continue ?
Download a directory from the Software Heritage Vault
You have requested the download of the directory with identifier swh:1:dir:52ec95fb47d65c214ed388293c06ccb8676ef4d6 as a standard tar.gz archive.
Are you sure you want to continue ?
Cook and download a revision from the Software Heritage Vault
You have requested the cooking of the history heading to revision with identifier swh:1:rev:b529da0913cdf6dfc184487d2f99b3a837407271 into a bare git archive.
Are you sure you want to continue ?
Download a revision from the Software Heritage Vault
You have requested the download of the history heading to revision with identifier swh:1:rev:b529da0913cdf6dfc184487d2f99b3a837407271 as a bare git archive.
Are you sure you want to continue ?
Invalid Email !
The provided email is not well-formed.
Download link has expired
The requested archive is no longer available for download from the Software Heritage Vault.
Do you want to cook it again ?
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.
An axiom-free formalization of well-founded relations, induction
| File | Mode | Size |
|---|---|---|
| Array.ec | -rw-r--r-- | 6.3 KB |
| BitEncoding.ec | -rw-r--r-- | 9.2 KB |
| BitWord.eca | -rw-r--r-- | 4.7 KB |
| FSet.ec | -rw-r--r-- | 24.3 KB |
| Int.ec | -rw-r--r-- | 14.1 KB |
| IntMin.ec | -rw-r--r-- | 1.7 KB |
| List.ec | -rw-r--r-- | 99.4 KB |
| Real.ec | -rw-r--r-- | 7.4 KB |
| Tuple.eca | -rw-r--r-- | 4.6 KB |
| Word.eca | -rw-r--r-- | 6.8 KB |
