Branch:
master
2971
3807_slowdown
3965_regression
3965_regression_2
4006_crash
CI-testing2
CI_fix10
CI_fix9
HashSet.merge
Int.pow_zero
IsDefEqFailureCache
LetExpr
MCtxM
MetavarContext
OfNatOption
Option.toMonad
PrivateWithMacroScopes
ac-refl-instances
add_bmod
add_missing_copyrights
advice_about_supportInterpreter
and_xor_distrib_left
apply_helpers
attribute_eq_refl
auto_aspirations
avoid_reserved
back_proj
back_simp
backport-2579-to-releases/v4.1.0
backport-2606-to-releases/v4.2.0
backport-3595-to-releases/v4.7.0
begin-dev-cycle-4.9.0
begin-dev-cycle-v4.4.0
begin-dev-cycle-v4.6.0
begin-dev-cycle-v4.7.0
begin_dev_cycle_v4.8.0
binder_predicates
bitVec_toNat_ofNat
bitblast
bitblast_cleanup
bitvec_authors
bitvec_int_add_mul_lemmas
bitvec_int_lemmas
bitvec_lemmas
bitvec_lemmas2
bitvec_ofNatLt
bitvec_simproc
bool_norm
bool_simps
boolasprop
build_win_issue
builtin_rpc_proc
bv_explicit_deceq_inst
bv_fin_lit_norm
bv_lit_match_perf
bv_no_std
bv_omega
canon_new
canon_univ
catchkernelexceptions
change
check_app_perf
check_tactic
ci-cancel
ci-full-build
ci-warn-as-error
clarify_copyright
cleanup_bitblast
cmake-flags
code_action
code_cleanup
coeOutParamIssue
coeOutParamIssue2
coe_fix
coefun_coehtc
collection_ops
completion_predicate
congr
congr_arg
convert
copyright_headers
copyright_typo
count-symbols
create_std_branches
csimpAttr
dany/low-level-code-gen
dbghelp
dead_code
deceqbeq
decide_cond_comment
decide_eq_true_eq
defEqCache
defeq_perf
defeq_perf2
defeq_perf_2
del_leftovers
delab_char_lit
deprecate_Option.toBool
deprecated_dot_notation
deprecation_dates
diag
diagnostics
diagnostics_improvements
digama_codeowners
disable_simproc
disable_win_tests
discr_tree_helpers
discrtree_unused_arg
doc-no-nightly
doc-prelude
docs/LawfulMonad
docs/Nat.gcd
docs/Ord
docs/Prod.mk
docs/add_decl_doc
dontresettccache
dsimproc
duplicate_theorems
elimOptParam_bug
eq_def
eqn_thm_nested_proofs
etaInst
eval_leak
ext
extern_prop_proj
extractLsb_flatten
false_or_by_contra2
false_or_by_contra_tests
fetch-nightly-with-mathlib
field_thm
finModDiv
finUsize
fix-c++-exc-again
fix1842
fix2095
fix2125
fix2173
fix2175
fix2188
fix2265
fix_2966
fix_3029
fix_3245
fix_hdiv_docstring
fix_hints_lt
fix_match_int
fix_mathlib_ci_rebase_suggestion
fix_most_recent_nightly_tag
fix_nat_class_defeq_simp
fix_release
fix_rfl
fix_run_meta
fixup-nightly
fixwindowsci
foldInfoTree
foldlits
fpil-readme
get_append
gh-readonly-queue/master/pr-3835-27c79cb6147b68c666292503919927055c923188
ground_modifier
guard_expr
hash64
hbv_find_join_points
heartbeats
improve_decide_error
initMacros
insertIf-linear
instances_diagnostics
int_norm
int_simproc
issue1218
issue1926
issue2321
issue2327
issue2552
issue2669
issue_2042
issue_2178
issue_2243
issue_2634
issue_2736
issue_2775
issue_2862
issue_2916
issue_3022
issue_3229
issue_3257
issue_3395
issue_3497
issue_3501
issue_3524
issue_3547
issue_3686
issue_3705
issue_3710
issue_3713
issue_3720
issue_3943
issues_summary.sh
ite-docs
jhx/reduceNat_fix
jhx/reduce_nat_fix
jhx/toArray
joachim/actionlint
joachim/argspacker
joachim/baseio_as_thunk
joachim/checkTargets
joachim/ci-comment-detectin
joachim/ci-quick-no-test
joachim/commit-convention-test
joachim/conv-calc
joachim/decreasing-omega
joachim/derecursifiers
joachim/doc-new-test
joachim/doc-recursive
joachim/doc-typo
joachim/docs-alternative
joachim/docs-head
joachim/docs-instantiateMVars
joachim/docs-mapM
joachim/docs-squash
joachim/drop_sizeof_get_lt
joachim/elim-info-let
joachim/eqnTypes-no-rfl
joachim/failed-to-unify
joachim/failed-to-unify2
joachim/failed-to-unify3
joachim/fix2925
joachim/flake-shell
joachim/float-recapp-common
joachim/funind-levels
joachim/funind-preserve-order
joachim/funind-reserved
joachim/funind-structural
joachim/funind-unqual-names
joachim/fuse-mkArgCongr
joachim/guardmsgs_space
joachim/guess-lex-badCassOn
joachim/guess-lex-shortcut
joachim/guesslex-diff
joachim/guesslex-expr
joachim/iff-rfl-attrib
joachim/ignore-test
joachim/induct-using-term
joachim/issue2260
joachim/issue2810
joachim/issue2810-take-two
joachim/issue3212
joachim/jq-syntax
joachim/manual-inhabited-sort
joachim/markdown-fixes-mvarctxt
joachim/matcherapp-transform
joachim/mem_upper_element
joachim/messagedata-isempty
joachim/mkArgCongr
joachim/more-test-2981
joachim/nat.toString
joachim/nat_repr_bench
joachim/nix-ci-trigger
joachim/no-funind-cmd
joachim/no-termination_by_core
joachim/noCasesOnApp
joachim/nofun
joachim/obsolete-comment
joachim/omega-error
joachim/omega-normalize-level
joachim/per-function-hints-before-where
joachim/pr-release-branch-or-tag
joachim/pr-release-fetch-base
joachim/pr-release-messages
joachim/pr-release-use-api
joachim/pr-release-🤦
joachim/pr-template
joachim/quick-ci
joachim/releases-markdown
joachim/remove-syntax
joachim/reserve-mutual-induct
joachim/reserved-name-error
joachim/resolveGlobal-docs
joachim/rfl-errors
joachim/rfl-no-kernel-defeq
joachim/shake-init
joachim/simp-prop
joachim/simpler-rw-terms
joachim/single-rfl
joachim/splitif-no-congr
joachim/stage0-label
joachim/stage0-queue-check
joachim/stage0-rebase-script
joachim/static-assert-warning
joachim/std-omega-reference
joachim/subst-bidi
joachim/subst-trace
joachim/tactics-in-ilean
joachim/termination-elab2
joachim/termination_binderIdent
joachim/termination_by_qmark
joachim/test-2982
joachim/typo-reursive
joachim/update-stage0
joachim/useIsAppOfArity
joachim/wf-irred
joachim/wf-irred2
joachim/wf-irred3
joachim/wf-irred4
joachim/wf-preprocess-beta
joachim/withReducible_eqnTypes
json_elab
json_sum
kmill-delab
lake-order-test-fix
lakeupdate230419
lazy_blacklist
lazy_discrtree_matchorder
lazy_disctree_cleanup
lazy_proj_defeq
lean-import-minimize
lean-no-shared
leanPosToLspPos
left_right
leo-henrik-doc
let_expr
letrec_in_thm_issue
liasolver_int_ediv_fix
librarySearch_tactic_default
library_search_fix_cache
library_search_release_note_update
library_search_test
libsearch_cleanup
libsearch_drop_nonspecific
linearity-erase
lint-prelude
linter-discover
localization_mwe
lychee-fail-false
macos-11
master
matchEq
matchRefactor
match_expr
match_expr_expected_type
match_expr_fix
match_expr_in_omega
match_expr_parser
match_expr_perf
match_int_issue
match_lit_issue
match_lit_issues
match_lit_regression
match_pattern_missing_test
match_using_fin_contra
mathlib_testing_logic
matrix-canceled
mhuisi-patch-1
mhuisi-patch-2
misctcfixes
missing-list-lemma
missingTicks
mkSimpContext
mk_theorem_bug
mod_mul
mod_norm
monadic_FindExpr
more_bitvec_missing
more_list_lemmas
most-recent-nightly-tag-permissions
move-elab-docstrings
name
nary_nomatch
nat_bitwise_support
native_edivmod
nightly
nightly-with-mathlib
nix-ci-update
no-cachix
no_inline_BitVec_cast
no_simp_msb_eq_decide
no_usize_simproc
nofun
nomatch_regression
nomatch_tac
norm_cast2
ofBoolListLE
ofsci
omegaCanon
omega_Bool_toNat
omega_bug
omega_fin
omega_ground
omega_mod_fix
omega_no_defeq
omega_rm_mkAppN_macro
omega_sup
option_docs
orphaned_tests_1
other_linter
parsec-linearity
parser_without_inline
perf_isDefEqProj
pp_fvar
pp_proofs_without_type
pr-release-agnostic
pr-release-logic
pr-release-origin
pred_eq_sub_one
pretty_options
printEqns
privateNameByMeta
proof_irrel_heq
protect_Int.add_right_inj
protected_bitvec
proto_expr_experiment
ptreq_cache
ptrset
race-cond
rcases
recRepr
red_attr_validate
reduceNatRegression
reducibility
refactor_SimpM
refactor_builtin_simproc
refactor_offset
refactor_simp
refine-mdbook-docs
refl_duplication
release-candidate
release_checklist
release_note_3507
release_notes_v4.6.1
release_ntoes
releases/v4.0.0-rc4
releases/v4.0.0-rc5
releases/v4.1.0
releases/v4.2.0
releases/v4.3.0
releases/v4.4.0
releases/v4.5.0
releases/v4.6.0
releases/v4.6.1
releases/v4.7.0
releases/v4.8.0
releases_note_2024-03-04
remove-gh-pages
remove_libsearch_cache
rename_Bool.toNat_le_one
rename_eqs
rename_i-macro
repeat
replace
replace_toExpr_int
reservedResolution
reserved_names
reset_reuse_bug
restore_4006
revert-2316-glibc-2.26
revert-2435-refine-natural-fix
revert-2648-cancel
revert_3020
revert_json_sum
rewrites_tactic
rfl_tactic
run-full-ci
run_cmd
rw_simp_issue
rw_uses_refl_not_applyRfl
rwa_tactic
rwissue
save
saved2
seal_unseal
semver-dash
set_lit_unexpand
set_literal
seval
shake_omega
shake_omega2
show_term
signExtend
simpIssues
simp_cache_perf
simp_congr_diag
simp_discharge_trace
simp_doc_decide_fix
simp_experiment
simp_ground
simp_ground_new
simp_inst_issue
simp_local_hyp
simp_missing_check
simp_proj_trans
simp_refactor
simp_result_bug
simp_skip_instance_implicit
simp_sub_add_cancel
simp_succ_eq_add_one
simp_toNat_mul
simp_trace_issues
simp_zetaDeltaIssue
simple_arrow
simpler_rc
simpler_rc2
simpler_rc3
simproc
simproc_char
simproc_doc_comments
simproc_docstring
simproc_erase
simproc_int_tonat
simproc_string
solve_by_elim_namespace
splitter_gen_code
stage0-graft/793cb2b8e3
stage0-graft/b762567174
std_command
stderrAsMessages-true
struct_cmd
struct_eq_bug
struct_simp_diag
succ_sub_succ_eq
swap_List.elem
symm_label_fixes
synth_perf
task-avoid-mt
tc_opt
tceta
test-summary
test_extern
test_extern_update
theorem_is_prop
toExprInsts
trace_at_kernel
trace_descr
trustCompiler_true
try_this
tsyntax_helpers
unfoldPartial
univ_approx
unsimp_of_length_zero
update-gh-script
upstream_Array_List_Init
upstream_BitVec
upstream_ByCases
upstream_CoeExt
upstream_Data_Fin_Iterate
upstream_List_TR
upstream_List_basic_ops_lemmas
upstream_LocalContext
upstream_MVarId.applyConst
upstream_NoMatch
upstream_Ordering
upstream_Std_Classes_LawfulMonad
upstream_Std_Data_Array_Init_Lemmas
upstream_Std_Data_Bool
upstream_Std_Data_Fin_Basic
upstream_Std_Data_Fin_Init_Lemmas
upstream_Std_Data_Fin_Lemmas
upstream_Std_Data_List_Init_Basic
upstream_Std_Data_List_Init_Lemmas
upstream_Std_Data_Nat_Bitwise
upstream_Std_Data_Nat_Lemmas
upstream_Std_Data_Prod_Lex
upstream_Std_option
upstream_Tactic
upstream_TermUnsafe
upstream_array_basic
upstream_dvd
upstream_exfalso
upstream_false_or_by_contra
upstream_getAppFnArgs
upstream_haveI
upstream_inequality_lemmas
upstream_int
upstream_int_init
upstream_library_search
upstream_logic
upstream_nat
upstream_nat_init
upstream_nat_recogniser
upstream_natcast
upstream_norm_cast_tests
upstream_set_notation
upstream_simpa
upstream_solve_by_elim
upstream_std_syntax_helpers
upstream_tests_2
use_nightly-testing-YYYY-MM-DD
using_omega
v4.3.0-release-notes
whnf-trace
windows-
withAssignableSyntheticOpaque_assumption
withLocation_doc_string
withtrace-except
zetaDelta
v4.8.0-rc1
v4.7.0-rc2
v4.7.0-rc1
v4.7.0
v4.6.1
v4.6.0-rc1
v4.6.0
v4.5.0-rc1
v4.5.0
v4.4.0-rc1
v4.4.0
v4.3.0-rc2
v4.3.0-rc1
v4.3.0
v4.2.0-rc4
v4.2.0-rc3
v4.2.0-rc2
v4.2.0-rc1
v4.2.0
v4.1.0-rc1
v4.1.0
v4.0.0-rc5
v4.0.0-rc4
v4.0.0-rc3
v4.0.0-rc2
v4.0.0-rc1
v4.0.0-m5
v4.0.0-m4
v4.0.0-m3
v4.0.0-m2
v4.0.0-m1
v4.0.0
cade2021
cade21
NFM2022
IJCAR20-LMCS
IJCAR20
IFL19
ICFP20
Leonardo de Moura
e362b50fa9
feat: add `seal` and `unseal` commands (#4053)
|
2 days ago | |
|---|---|---|
| .. | ||
| bench | 4f50544242 chore: Nat.repr microbenchmark (#3888) | 2 weeks ago |
| compiler | 3b4b2cc89d fix: do not dllexport symbols in core static libraries (#3601) | 1 month ago |
| elabissues | 1118931516 feat: add bitwise operations to reduceNat? and kernel (#3134) | 3 months ago |
| ir | 42e6214a42 feat: lake: GNU/BSD OS detection in test scripts (#3180) | 3 months ago |
| lean | e362b50fa9 feat: add `seal` and `unseal` commands (#4053) | 2 days ago |
| pkg | 2df35360ee feat: validate reducibility attribute setting (#4052) | 2 days ago |
| playground | 01104cc81e chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508) | 2 months ago |
| plugin | 3b4b2cc89d fix: do not dllexport symbols in core static libraries (#3601) | 1 month ago |
| simpperf | 57e05af9da feat: add `simp` benchmark | 3 years ago |
| .gitignore | 10253e89ea chore: move bin/ and .oleans into build directory | 4 years ago |
| common.sh | f165414e13 fix: use -O3 for LLVM tests in common.sh | 6 months ago |
| lean-toolchain | 3a0edd05e6 doc: VS Code dev setup (#2961) | 5 months ago |