mirror of
https://git.FreeBSD.org/ports.git
synced 2024-11-18 00:10:04 +00:00
math/lean4: update 4.11.0 → 4.12.0
This commit is contained in:
Yuri Victorovich
parent
30cc2ea76f
commit
fec276899d
@ -1,7 +1,6 @@
|
||||
PORTNAME= lean4
|
||||
DISTVERSIONPREFIX= v
|
||||
DISTVERSION= 4.11.0
|
||||
PORTREVISION= 1
|
||||
DISTVERSION= 4.12.0
|
||||
CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
|
||||
|
||||
MAINTAINER= yuri@FreeBSD.org
|
||||
@ -14,8 +13,11 @@ LICENSE_FILE= ${WRKSRC}/LICENSE
|
||||
BROKEN_armv7= compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory
|
||||
BROKEN_i386= linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
|
||||
|
||||
BUILD_DEPENDS= bash:shells/bash
|
||||
LIB_DEPENDS= libgmp.so:math/gmp
|
||||
BUILD_DEPENDS= bash:shells/bash \
|
||||
cadical:math/cadical
|
||||
LIB_DEPENDS= libgmp.so:math/gmp \
|
||||
libuv.so:devel/libuv
|
||||
RUN_DEPENDS= cadical:math/cadical
|
||||
|
||||
USES= cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project
|
||||
|
||||
@ -43,6 +45,8 @@ post-install:
|
||||
@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
|
||||
# remove stray files
|
||||
@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
|
||||
# remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603
|
||||
@${RM} ${STAGEDIR}${PREFIX}/bin/cadical
|
||||
# strip binaries
|
||||
@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
|
||||
bin/lake \
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
TIMESTAMP = 1725254182
|
||||
SHA256 (leanprover-lean4-v4.11.0_GH0.tar.gz) = 8b7fc8e71e107250c7bbf911eb1f450379d874857a26236577aaa624dd5962b5
|
||||
SIZE (leanprover-lean4-v4.11.0_GH0.tar.gz) = 25790812
|
||||
TIMESTAMP = 1727897287
|
||||
SHA256 (leanprover-lean4-v4.12.0_GH0.tar.gz) = 409f623eb9044b3b025951415dfa0db531ed29056a5fba5d556394ad9435e62b
|
||||
SIZE (leanprover-lean4-v4.12.0_GH0.tar.gz) = 27334919
|
||||
|
||||
@ -5,6 +5,7 @@ bin/leanmake
|
||||
include/lean/config.h
|
||||
include/lean/lean.h
|
||||
include/lean/lean_gmp.h
|
||||
include/lean/lean_libuv.h
|
||||
include/lean/version.h
|
||||
lib/lean/Init.ilean
|
||||
lib/lean/Init.olean
|
||||
@ -156,6 +157,8 @@ lib/lean/Init/Data/Int/Gcd.ilean
|
||||
lib/lean/Init/Data/Int/Gcd.olean
|
||||
lib/lean/Init/Data/Int/Lemmas.ilean
|
||||
lib/lean/Init/Data/Int/Lemmas.olean
|
||||
lib/lean/Init/Data/Int/LemmasAux.ilean
|
||||
lib/lean/Init/Data/Int/LemmasAux.olean
|
||||
lib/lean/Init/Data/Int/Order.ilean
|
||||
lib/lean/Init/Data/Int/Order.olean
|
||||
lib/lean/Init/Data/Int/Pow.ilean
|
||||
@ -192,12 +195,26 @@ lib/lean/Init/Data/List/Nat/Pairwise.ilean
|
||||
lib/lean/Init/Data/List/Nat/Pairwise.olean
|
||||
lib/lean/Init/Data/List/Nat/Range.ilean
|
||||
lib/lean/Init/Data/List/Nat/Range.olean
|
||||
lib/lean/Init/Data/List/Nat/Sublist.ilean
|
||||
lib/lean/Init/Data/List/Nat/Sublist.olean
|
||||
lib/lean/Init/Data/List/Nat/TakeDrop.ilean
|
||||
lib/lean/Init/Data/List/Nat/TakeDrop.olean
|
||||
lib/lean/Init/Data/List/Notation.ilean
|
||||
lib/lean/Init/Data/List/Notation.olean
|
||||
lib/lean/Init/Data/List/Pairwise.ilean
|
||||
lib/lean/Init/Data/List/Pairwise.olean
|
||||
lib/lean/Init/Data/List/Perm.ilean
|
||||
lib/lean/Init/Data/List/Perm.olean
|
||||
lib/lean/Init/Data/List/Range.ilean
|
||||
lib/lean/Init/Data/List/Range.olean
|
||||
lib/lean/Init/Data/List/Sort.ilean
|
||||
lib/lean/Init/Data/List/Sort.olean
|
||||
lib/lean/Init/Data/List/Sort/Basic.ilean
|
||||
lib/lean/Init/Data/List/Sort/Basic.olean
|
||||
lib/lean/Init/Data/List/Sort/Impl.ilean
|
||||
lib/lean/Init/Data/List/Sort/Impl.olean
|
||||
lib/lean/Init/Data/List/Sort/Lemmas.ilean
|
||||
lib/lean/Init/Data/List/Sort/Lemmas.olean
|
||||
lib/lean/Init/Data/List/Sublist.ilean
|
||||
lib/lean/Init/Data/List/Sublist.olean
|
||||
lib/lean/Init/Data/List/TakeDrop.ilean
|
||||
@ -256,6 +273,8 @@ lib/lean/Init/Data/Option/Lemmas.ilean
|
||||
lib/lean/Init/Data/Option/Lemmas.olean
|
||||
lib/lean/Init/Data/Ord.ilean
|
||||
lib/lean/Init/Data/Ord.olean
|
||||
lib/lean/Init/Data/PLift.ilean
|
||||
lib/lean/Init/Data/PLift.olean
|
||||
lib/lean/Init/Data/Prod.ilean
|
||||
lib/lean/Init/Data/Prod.olean
|
||||
lib/lean/Init/Data/Queue.ilean
|
||||
@ -296,6 +315,8 @@ lib/lean/Init/Data/UInt/Lemmas.ilean
|
||||
lib/lean/Init/Data/UInt/Lemmas.olean
|
||||
lib/lean/Init/Data/UInt/Log2.ilean
|
||||
lib/lean/Init/Data/UInt/Log2.olean
|
||||
lib/lean/Init/Data/ULift.ilean
|
||||
lib/lean/Init/Data/ULift.olean
|
||||
lib/lean/Init/Dynamic.ilean
|
||||
lib/lean/Init/Dynamic.olean
|
||||
lib/lean/Init/Ext.ilean
|
||||
@ -946,8 +967,6 @@ lib/lean/Lean/Data/OpenDecl.ilean
|
||||
lib/lean/Lean/Data/OpenDecl.olean
|
||||
lib/lean/Lean/Data/Options.ilean
|
||||
lib/lean/Lean/Data/Options.olean
|
||||
lib/lean/Lean/Data/Parsec.ilean
|
||||
lib/lean/Lean/Data/Parsec.olean
|
||||
lib/lean/Lean/Data/PersistentArray.ilean
|
||||
lib/lean/Lean/Data/PersistentArray.olean
|
||||
lib/lean/Lean/Data/PersistentHashMap.ilean
|
||||
@ -1116,12 +1135,16 @@ lib/lean/Lean/Elab/PreDefinition.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Basic.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/Basic.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/EqUnfold.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/EqUnfold.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Eqns.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/Eqns.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Main.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/Main.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/MkInhabitant.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/MkInhabitant.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Structural.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/Structural.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/Structural/BRecOn.ilean
|
||||
@ -1150,6 +1173,8 @@ lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF/Basic.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF/Basic.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF/Eqns.olean
|
||||
lib/lean/Lean/Elab/PreDefinition/WF/Fix.ilean
|
||||
@ -1188,8 +1213,42 @@ lib/lean/Lean/Elab/SyntheticMVars.ilean
|
||||
lib/lean/Lean/Elab/SyntheticMVars.olean
|
||||
lib/lean/Lean/Elab/Tactic.ilean
|
||||
lib/lean/Lean/Elab/Tactic.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/External.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/External.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.olean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.olean
|
||||
lib/lean/Lean/Elab/Tactic/Basic.ilean
|
||||
lib/lean/Lean/Elab/Tactic/Basic.olean
|
||||
lib/lean/Lean/Elab/Tactic/BoolToPropSimps.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BoolToPropSimps.olean
|
||||
lib/lean/Lean/Elab/Tactic/BuiltinTactic.ilean
|
||||
lib/lean/Lean/Elab/Tactic/BuiltinTactic.olean
|
||||
lib/lean/Lean/Elab/Tactic/Cache.ilean
|
||||
@ -1290,6 +1349,8 @@ lib/lean/Lean/Elab/Tactic/Unfold.ilean
|
||||
lib/lean/Lean/Elab/Tactic/Unfold.olean
|
||||
lib/lean/Lean/Elab/Term.ilean
|
||||
lib/lean/Lean/Elab/Term.olean
|
||||
lib/lean/Lean/Elab/Time.ilean
|
||||
lib/lean/Lean/Elab/Time.olean
|
||||
lib/lean/Lean/Elab/Util.ilean
|
||||
lib/lean/Lean/Elab/Util.olean
|
||||
lib/lean/Lean/Environment.ilean
|
||||
@ -1852,6 +1913,8 @@ lib/lean/Lean/Util/MonadBacktrack.ilean
|
||||
lib/lean/Lean/Util/MonadBacktrack.olean
|
||||
lib/lean/Lean/Util/MonadCache.ilean
|
||||
lib/lean/Lean/Util/MonadCache.olean
|
||||
lib/lean/Lean/Util/NumApps.ilean
|
||||
lib/lean/Lean/Util/NumApps.olean
|
||||
lib/lean/Lean/Util/NumObjs.ilean
|
||||
lib/lean/Lean/Util/NumObjs.olean
|
||||
lib/lean/Lean/Util/OccursCheck.ilean
|
||||
@ -1934,8 +1997,6 @@ lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Perm.ilean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Perm.olean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean
|
||||
lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean
|
||||
lib/lean/Std/Data/DHashMap/Internal/Model.ilean
|
||||
@ -1976,14 +2037,246 @@ lib/lean/Std/Data/HashSet/Raw.ilean
|
||||
lib/lean/Std/Data/HashSet/Raw.olean
|
||||
lib/lean/Std/Data/HashSet/RawLemmas.ilean
|
||||
lib/lean/Std/Data/HashSet/RawLemmas.olean
|
||||
lib/lean/Std/Internal.ilean
|
||||
lib/lean/Std/Internal.olean
|
||||
lib/lean/Std/Internal/Parsec.ilean
|
||||
lib/lean/Std/Internal/Parsec.olean
|
||||
lib/lean/Std/Internal/Parsec/Basic.ilean
|
||||
lib/lean/Std/Internal/Parsec/Basic.olean
|
||||
lib/lean/Std/Internal/Parsec/ByteArray.ilean
|
||||
lib/lean/Std/Internal/Parsec/ByteArray.olean
|
||||
lib/lean/Std/Internal/Parsec/String.ilean
|
||||
lib/lean/Std/Internal/Parsec/String.olean
|
||||
lib/lean/Std/Sat.ilean
|
||||
lib/lean/Std/Sat.olean
|
||||
lib/lean/Std/Sat/AIG.ilean
|
||||
lib/lean/Std/Sat/AIG.olean
|
||||
lib/lean/Std/Sat/AIG/Basic.ilean
|
||||
lib/lean/Std/Sat/AIG/Basic.olean
|
||||
lib/lean/Std/Sat/AIG/CNF.ilean
|
||||
lib/lean/Std/Sat/AIG/CNF.olean
|
||||
lib/lean/Std/Sat/AIG/Cached.ilean
|
||||
lib/lean/Std/Sat/AIG/Cached.olean
|
||||
lib/lean/Std/Sat/AIG/CachedGates.ilean
|
||||
lib/lean/Std/Sat/AIG/CachedGates.olean
|
||||
lib/lean/Std/Sat/AIG/CachedGatesLemmas.ilean
|
||||
lib/lean/Std/Sat/AIG/CachedGatesLemmas.olean
|
||||
lib/lean/Std/Sat/AIG/CachedLemmas.ilean
|
||||
lib/lean/Std/Sat/AIG/CachedLemmas.olean
|
||||
lib/lean/Std/Sat/AIG/If.ilean
|
||||
lib/lean/Std/Sat/AIG/If.olean
|
||||
lib/lean/Std/Sat/AIG/LawfulOperator.ilean
|
||||
lib/lean/Std/Sat/AIG/LawfulOperator.olean
|
||||
lib/lean/Std/Sat/AIG/LawfulVecOperator.ilean
|
||||
lib/lean/Std/Sat/AIG/LawfulVecOperator.olean
|
||||
lib/lean/Std/Sat/AIG/Lemmas.ilean
|
||||
lib/lean/Std/Sat/AIG/Lemmas.olean
|
||||
lib/lean/Std/Sat/AIG/RefVec.ilean
|
||||
lib/lean/Std/Sat/AIG/RefVec.olean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator.ilean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator.olean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Fold.ilean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Fold.olean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Map.ilean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Map.olean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Zip.ilean
|
||||
lib/lean/Std/Sat/AIG/RefVecOperator/Zip.olean
|
||||
lib/lean/Std/Sat/AIG/Relabel.ilean
|
||||
lib/lean/Std/Sat/AIG/Relabel.olean
|
||||
lib/lean/Std/Sat/AIG/RelabelNat.ilean
|
||||
lib/lean/Std/Sat/AIG/RelabelNat.olean
|
||||
lib/lean/Std/Sat/CNF.ilean
|
||||
lib/lean/Std/Sat/CNF.olean
|
||||
lib/lean/Std/Sat/CNF/Basic.ilean
|
||||
lib/lean/Std/Sat/CNF/Basic.olean
|
||||
lib/lean/Std/Sat/CNF/Dimacs.ilean
|
||||
lib/lean/Std/Sat/CNF/Dimacs.olean
|
||||
lib/lean/Std/Sat/CNF/Literal.ilean
|
||||
lib/lean/Std/Sat/CNF/Literal.olean
|
||||
lib/lean/Std/Sat/CNF/Relabel.ilean
|
||||
lib/lean/Std/Sat/CNF/Relabel.olean
|
||||
lib/lean/Std/Sat/CNF/RelabelFin.ilean
|
||||
lib/lean/Std/Sat/CNF/RelabelFin.olean
|
||||
lib/lean/Std/Tactic.ilean
|
||||
lib/lean/Std/Tactic.olean
|
||||
lib/lean/Std/Tactic/BVDecide.ilean
|
||||
lib/lean/Std/Tactic/BVDecide.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Actions.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Actions.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.olean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/LRAT/Parser.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/BitVec.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/BitVec.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Bool.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Bool.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Equal.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Equal.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Prop.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Normalize/Prop.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Reflect.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Reflect.olean
|
||||
lib/lean/Std/Tactic/BVDecide/Syntax.ilean
|
||||
lib/lean/Std/Tactic/BVDecide/Syntax.olean
|
||||
lib/lean/libInit.a
|
||||
lib/lean/libInit_shared.so
|
||||
lib/lean/libLake.a
|
||||
lib/lean/libLean.a
|
||||
lib/lean/libStd.a
|
||||
lib/lean/libleancpp.a
|
||||
lib/lean/libleanmanifest.a
|
||||
lib/lean/libleanrt.a
|
||||
lib/lean/libleanshared.so
|
||||
lib/lean/libleanshared_1.so
|
||||
share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Init.lean
|
||||
%%DATADIR%%/src/lean/Init/BinderPredicates.lean
|
||||
@ -2060,6 +2353,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/DivModLemmas.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/LemmasAux.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/Order.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Int/Pow.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List.lean
|
||||
@ -2078,9 +2372,16 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Nat/Sublist.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Notation.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Perm.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Range.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Sort.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Sort/Basic.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Sort/Impl.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Sort/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Sublist.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/List/Zip.lean
|
||||
@ -2110,6 +2411,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Init/Data/Option/Instances.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Option/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Ord.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/PLift.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Prod.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Queue.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/Random.lean
|
||||
@ -2130,6 +2432,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean
|
||||
%%DATADIR%%/src/lean/Init/Data/ULift.lean
|
||||
%%DATADIR%%/src/lean/Init/Dynamic.lean
|
||||
%%DATADIR%%/src/lean/Init/Ext.lean
|
||||
%%DATADIR%%/src/lean/Init/GetElem.lean
|
||||
@ -2327,7 +2630,6 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Data/NameTrie.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/OpenDecl.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/Options.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/Parsec.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/PersistentArray.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/PersistentHashMap.lean
|
||||
%%DATADIR%%/src/lean/Lean/Data/PersistentHashSet.lean
|
||||
@ -2412,9 +2714,11 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PatternVar.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Basic.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/EqUnfold.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Eqns.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Main.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/MkInhabitant.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/BRecOn.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean
|
||||
@ -2429,6 +2733,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Basic.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/GuessLex.lean
|
||||
@ -2448,7 +2753,24 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Syntax.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/SyntheticMVars.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/External.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/Basic.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BoolToPropSimps.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/BuiltinTactic.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/Cache.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/Calc.lean
|
||||
@ -2499,6 +2821,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/Symm.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Tactic/Unfold.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Term.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Time.lean
|
||||
%%DATADIR%%/src/lean/Lean/Elab/Util.lean
|
||||
%%DATADIR%%/src/lean/Lean/Environment.lean
|
||||
%%DATADIR%%/src/lean/Lean/Eval.lean
|
||||
@ -2781,6 +3104,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/MonadBacktrack.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/MonadCache.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/NumApps.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/NumObjs.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/OccursCheck.lean
|
||||
%%DATADIR%%/src/lean/Lean/Util/PPExt.lean
|
||||
@ -2823,7 +3147,6 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Perm.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean
|
||||
@ -2844,6 +3167,121 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean
|
||||
%%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Internal.lean
|
||||
%%DATADIR%%/src/lean/Std/Internal/Parsec.lean
|
||||
%%DATADIR%%/src/lean/Std/Internal/Parsec/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Internal/Parsec/ByteArray.lean
|
||||
%%DATADIR%%/src/lean/Std/Internal/Parsec/String.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/CNF.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/Cached.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/CachedGates.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/CachedLemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/If.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/LawfulOperator.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RefVec.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/Relabel.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/AIG/RelabelNat.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF/Dimacs.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF/Literal.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF/Relabel.lean
|
||||
%%DATADIR%%/src/lean/Std/Sat/CNF/RelabelFin.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Instance.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATChecker.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/PosFin.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Prop.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Reflect.lean
|
||||
%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Syntax.lean
|
||||
%%DATADIR%%/src/lean/lake/Lake.lean
|
||||
%%DATADIR%%/src/lean/lake/Lake/Build.lean
|
||||
%%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
|
||||
@ -2988,6 +3426,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/lake/tests/clone/test/Main.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/clone/test/lakefile.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/driver/Test.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/driver/build.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/driver/dep-invalid.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/driver/dep-unknown.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/driver/dep.lean
|
||||
@ -3054,6 +3493,7 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/lake/tests/precompileArgs/lakefile.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/reservoirConfig/lakefile.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/reversion/Main.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean
|
||||
@ -3062,3 +3502,4 @@ share/lean/lean.mk
|
||||
%%DATADIR%%/src/lean/lake/tests/trace/Foo.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean
|
||||
%%DATADIR%%/src/lean/lake/tests/versionTags/lakefile.lean
|
||||
|
||||
Loading…
Reference in New Issue
Block a user