https://github.com/EasyCrypt/easycrypt
History
Tip revision: 863066bded664a5e2aba7f89c4fb7bc2afd0e28d authored by Pierre-Yves Strub on 23 September 2015, 08:28 UTC
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Tip revision: 863066b
File Mode Size
phl
system
ec.ml -rw-r--r-- 10.2 KB
ecAlgTactic.ml -rw-r--r-- 8.5 KB
ecAlgTactic.mli -rw-r--r-- 1.5 KB
ecAlgebra.ml -rw-r--r-- 13.8 KB
ecAlgebra.mli -rw-r--r-- 4.8 KB
ecBaseLogic.ml -rw-r--r-- 791 bytes
ecBigInt.ml -rw-r--r-- 2.1 KB
ecBigInt.mli -rw-r--r-- 1.7 KB
ecCommands.ml -rw-r--r-- 27.7 KB
ecCommands.mli -rw-r--r-- 1.8 KB
ecCoreFol.ml -rw-r--r-- 50.0 KB
ecCoreFol.mli -rw-r--r-- 12.9 KB
ecCoreGoal.ml -rw-r--r-- 34.9 KB
ecCoreGoal.mli -rw-r--r-- 15.8 KB
ecCoreHiPhl.ml -rw-r--r-- 2.5 KB
ecCoreHiPhl.mli -rw-r--r-- 898 bytes
ecCoreLib.ml -rw-r--r-- 6.0 KB
ecCoreLib.mli -rw-r--r-- 4.2 KB
ecDecl.ml -rw-r--r-- 7.6 KB
ecDecl.mli -rw-r--r-- 4.1 KB
ecEnv.ml -rw-r--r-- 98.2 KB
ecEnv.mli -rw-r--r-- 13.6 KB
ecField.ml -rw-r--r-- 6.2 KB
ecField.mli -rw-r--r-- 795 bytes
ecFol.ml -rw-r--r-- 21.5 KB
ecFol.mli -rw-r--r-- 5.2 KB
ecFortune.ml -rw-r--r-- 1.8 KB
ecFortune.mli -rw-r--r-- 401 bytes
ecGState.ml -rw-r--r-- 3.4 KB
ecGState.mli -rw-r--r-- 1.5 KB
ecHiGoal.ml -rw-r--r-- 45.9 KB
ecHiGoal.mli -rw-r--r-- 3.6 KB
ecHiInductive.ml -rw-r--r-- 15.0 KB
ecHiInductive.mli -rw-r--r-- 2.4 KB
ecHiTacticals.ml -rw-r--r-- 13.3 KB
ecHiTacticals.mli -rw-r--r-- 596 bytes
ecIdent.ml -rw-r--r-- 1.8 KB
ecIdent.mli -rw-r--r-- 1.4 KB
ecInductive.ml -rw-r--r-- 6.8 KB
ecInductive.mli -rw-r--r-- 2.0 KB
ecIo.ml -rw-r--r-- 6.8 KB
ecIo.mli -rw-r--r-- 1.2 KB
ecLexer.mll -rw-r--r-- 16.5 KB
ecLoader.ml -rw-r--r-- 4.6 KB
ecLoader.mli -rw-r--r-- 781 bytes
ecLocation.ml -rw-r--r-- 2.8 KB
ecLocation.mli -rw-r--r-- 1.5 KB
ecLowGoal.ml -rw-r--r-- 52.1 KB
ecLowGoal.mli -rw-r--r-- 8.5 KB
ecLowPhlGoal.ml -rw-r--r-- 21.1 KB
ecMaps.ml -rw-r--r-- 3.7 KB
ecMatching.ml -rw-r--r-- 25.5 KB
ecMatching.mli -rw-r--r-- 5.1 KB
ecMemory.ml -rw-r--r-- 3.8 KB
ecMemory.mli -rw-r--r-- 2.7 KB
ecModules.ml -rw-r--r-- 20.0 KB
ecModules.mli -rw-r--r-- 6.5 KB
ecOptions.ml -rw-r--r-- 11.1 KB
ecOptions.mli -rw-r--r-- 1.2 KB
ecPException.ml -rw-r--r-- 1.6 KB
ecPException.mli -rw-r--r-- 497 bytes
ecPV.ml -rw-r--r-- 33.8 KB
ecPV.mli -rw-r--r-- 5.6 KB
ecParser.mly -rw-r--r-- 72.7 KB
ecParsetree.ml -rw-r--r-- 25.6 KB
ecPath.ml -rw-r--r-- 9.3 KB
ecPath.mli -rw-r--r-- 4.0 KB
ecPrinting.ml -rw-r--r-- 85.2 KB
ecPrinting.mli -rw-r--r-- 3.1 KB
ecProofTerm.ml -rw-r--r-- 25.9 KB
ecProofTerm.mli -rw-r--r-- 4.7 KB
ecProofTyping.ml -rw-r--r-- 7.5 KB
ecProofTyping.mli -rw-r--r-- 3.4 KB
ecProvers.ml -rw-r--r-- 15.4 KB
ecProvers.mli -rw-r--r-- 1.9 KB
ecReduction.ml -rw-r--r-- 25.4 KB
ecReduction.mli -rw-r--r-- 2.0 KB
ecRing.ml -rw-r--r-- 13.6 KB
ecRing.mli -rw-r--r-- 2.3 KB
ecScope.ml -rw-r--r-- 89.9 KB
ecScope.mli -rw-r--r-- 6.8 KB
ecSearch.ml -rw-r--r-- 2.4 KB
ecSearch.mli -rw-r--r-- 375 bytes
ecSection.ml -rw-r--r-- 14.3 KB
ecSection.mli -rw-r--r-- 1.8 KB
ecSmt.ml -rw-r--r-- 48.1 KB
ecSmt.mli -rw-r--r-- 299 bytes
ecStrongRing.ml -rw-r--r-- 11.2 KB
ecSubst.ml -rw-r--r-- 19.3 KB
ecSubst.mli -rw-r--r-- 2.4 KB
ecSymbols.ml -rw-r--r-- 2.7 KB
ecSymbols.mli -rw-r--r-- 1.5 KB
ecTerminal.ml -rw-r--r-- 6.7 KB
ecTerminal.mli -rw-r--r-- 964 bytes
ecThCloning.ml -rw-r--r-- 17.2 KB
ecThCloning.mli -rw-r--r-- 2.4 KB
ecTheory.ml -rw-r--r-- 2.8 KB
ecTheory.mli -rw-r--r-- 2.2 KB
ecTypeClass.ml -rw-r--r-- 2.4 KB
ecTypeClass.mli -rw-r--r-- 754 bytes
ecTypes.ml -rw-r--r-- 27.0 KB
ecTypes.mli -rw-r--r-- 7.3 KB
ecTyping.ml -rw-r--r-- 82.7 KB
ecTyping.mli -rw-r--r-- 5.7 KB
ecUFind.ml -rw-r--r-- 5.5 KB
ecUFind.mli -rw-r--r-- 1.7 KB
ecUid.ml -rw-r--r-- 2.2 KB
ecUid.mli -rw-r--r-- 1.2 KB
ecUnify.ml -rw-r--r-- 13.5 KB
ecUnify.mli -rw-r--r-- 1.7 KB
ecUtils.ml -rw-r--r-- 19.1 KB
ecUtils.mli -rw-r--r-- 10.1 KB
ecVersion.ml -rw-r--r-- 675 bytes
ecVersion.mli -rw-r--r-- 460 bytes
ecWhy3Conv.ml -rw-r--r-- 6.2 KB
ecWhy3Conv.mli -rw-r--r-- 558 bytes

back to top