Skip to main content
  • Home
  • Development
  • Documentation
  • Donate
  • Operational login
  • Browse the archive

swh logo
SoftwareHeritage
Software
Heritage
Archive
Features
  • Search

  • Downloads

  • Save code now

  • Add forge now

  • Help

https://github.com/EasyCrypt/easycrypt
08 March 2026, 21:21:22 UTC
  • Code
  • Branches (46)
  • Releases (9)
  • Visits
Revision a7213928cab3aa334d0bdaf73f48c69400e08982 authored by François Dupressoir on 06 November 2019, 20:46:14 UTC, committed by François Dupressoir on 06 December 2019, 09:54:54 UTC
[SmtMap] add has, find and some lemmas
these are focused on a specific proof and deserve expanding, fleshing out and cleaning up
1 parent 89e35d1
  • Files
  • Changes
    • Branches
    • Releases
    • HEAD
    • refs/heads/aprhl
    • refs/heads/arrays
    • refs/heads/bdep_ecCircuitsRefactor
    • refs/heads/bdep_merge_conseq_fix
    • refs/heads/bdep_mldsa_correctness
    • refs/heads/ci-build-docker-test-on-release
    • refs/heads/comm-algebra
    • refs/heads/coupling-rnd-tactics
    • refs/heads/delayed-couplings
    • refs/heads/deploy-fix-#154
    • refs/heads/deploy-quantum-upgrade
    • refs/heads/deploy-tc
    • refs/heads/distr-matrix
    • refs/heads/doc-seq-tactic
    • refs/heads/doc-types
    • refs/heads/doc-while-tactic
    • refs/heads/dynmatrix-stability
    • refs/heads/eHoare-example
    • refs/heads/eval-pwhile
    • refs/heads/expr-fold
    • refs/heads/feature_procchange_framing
    • refs/heads/feature_signed_modP
    • refs/heads/fix-142
    • refs/heads/fix-729
    • refs/heads/fix_opsel_error_printing
    • refs/heads/fmap-fold
    • refs/heads/improve_nix_flake
    • refs/heads/indexed-types
    • refs/heads/jasmin-in-ci
    • refs/heads/latest
    • refs/heads/main
    • refs/heads/ocaml-5
    • refs/heads/ois-refactoring
    • refs/heads/perms-group
    • refs/heads/polydiv
    • refs/heads/pose-match-fix
    • refs/heads/r2022.04-01
    • refs/heads/release
    • refs/heads/setoidrw
    • refs/heads/softcode-memories
    • refs/heads/subtypes
    • refs/heads/theory_finite_field
    • refs/heads/uptobad_warnings
    • refs/heads/vscode
    • refs/heads/yaeasypqc
    • refs/tags/r2024.09
    • a7213928cab3aa334d0bdaf73f48c69400e08982
    • r2026.02
    • r2025.11
    • r2025.10
    • r2025.08
    • r2025.03
    • r2025.02
    • r2024.01
    • r2023.09
    • r2022.04
  • f841002
  • /
History
Cook and download a directory from the Software Heritage Vault

You have requested the cooking of the directory with identifier swh:1:dir:f841002b89e71ed3577dc73b816811f6ccb42d0f 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:f841002b89e71ed3577dc73b816811f6ccb42d0f 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:a7213928cab3aa334d0bdaf73f48c69400e08982 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:a7213928cab3aa334d0bdaf73f48c69400e08982 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 ?

Save again
Take a new snapshot of a software origin

If the archived software origin currently browsed is not synchronized with its upstream version (for instance when new commits have been issued), you can explicitly request Software Heritage to take a new snapshot of it.

Use the form below to proceed. Once a request has been submitted and accepted, it will be processed as soon as possible. You can then check its processing state by visiting this dedicated page.
swh spinner

Processing "take a new snapshot" request ...

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.

  • revision
  • directory
  • snapshot
origin badgerevision badge
swh:1:rev:a7213928cab3aa334d0bdaf73f48c69400e08982
origin badgedirectory badge
swh:1:dir:f841002b89e71ed3577dc73b816811f6ccb42d0f
origin badgesnapshot badge
swh:1:snp:3263266885d5cf55dbd7799e62b959841a8b1e8c

This interface enables to generate software citations, provided that the root directory of browsed objects contains a citation.cff or codemeta.json file.
Select below a type of object currently browsed in order to generate citations for them.

  • revision
  • directory
  • snapshot
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Tip revision: a7213928cab3aa334d0bdaf73f48c69400e08982 authored by François Dupressoir on 06 November 2019, 20:46:14 UTC
[SmtMap] add has, find and some lemmas
Tip revision: a721392
FileModeSize
config
examples
lint
scripts
src
theories
.dir-locals.el -rw-r--r--285 bytes
.gitignore -rw-r--r--515 bytes
.merlin -rw-r--r--241 bytes
.travis.yml -rw-r--r--2.0 KB
COPYRIGHT -rw-r--r--581 bytes
COPYRIGHT.yaml -rw-r--r--596 bytes
MANIFEST -rw-r--r--596 bytes
Makefile -rw-r--r--4.8 KB
Makefile.system -rw-r--r--555 bytes
README.md -rw-r--r--8.3 KB
_tags -rw-r--r--812 bytes
default.nix -rw-r--r--225 bytes
myocamlbuild.ml -rw-r--r--2.3 KB

The diff you're trying to view is too large. Only the first 1000 changed files have been loaded.
Showing with 0 additions and 0 deletions (0 / 0 diffs computed)
swh spinner

Computing file changes ...

README.md

swh spinner

Loading README.md ...

back to top

Software Heritage — Copyright (C) 2015–2026, The Software Heritage developers. License: GNU AGPLv3+.
The source code of Software Heritage itself is available on our development forge.
The source code files archived by Software Heritage are available under their own copyright and licenses.
Terms of use: Archive access, API— Content policy— Contact— JavaScript license information— Web API