max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/run
History
Leonardo de Moura 4ee131981d feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.

The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
  | stop : HasType 0 (ty :: ctx) ty
  | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty

inductive Sublist : List α → List α → Prop
  | slnil : Sublist [] []
  | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)

inductive Lst : Type u → Type u
  | nil  : Lst α
  | cons : α → Lst α → Lst α
```

TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.

TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
2022-03-08 17:56:34 -08:00
..
.gitignore fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
28.lean
29.lean
34.lean
52_lean3.lean
91_lean3.lean
102_lean3.lean
108.lean
111.lean
121.lean
125.lean chore: fix tests 2020-12-18 11:21:30 -08:00
175.lean
229.lean
262.lean feat: add support for guessing (very) simple WF relations 2022-03-02 11:52:00 -08:00
269.lean
270.lean chore: fix tests 2021-05-04 15:42:03 -07:00
280.lean test: add "discriminant refinement" tests 2021-03-24 19:10:50 -07:00
281.lean
282.lean
303.lean
305.lean feat: don't allow whitespaces between . and field name 2021-04-05 07:11:14 -07:00
310.lean
319.lean
326.lean
327.lean feat: closes #327 2021-03-24 12:29:33 -07:00
329.lean
335.lean
337.lean
338.lean
341.lean
382.lean feat: use binop% to define arith operators 2021-04-30 19:40:45 -07:00
387.lean chore: fix tests 2021-09-16 10:29:38 -07:00
394.lean chore: fix tests 2021-08-07 13:22:58 -07:00
436.lean feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
436_lean3.lean
441.lean test: closes #441 2021-05-15 20:37:48 -07:00
447_lean3.lean
452.lean fix: fixes #452 2021-05-10 17:28:10 -07:00
457.lean fix: fixes #457 2021-05-12 20:45:54 -07:00
461a.lean feat: take auto params into account in the structure instance notation 2021-07-27 15:49:23 -07:00
461b.lean fix: bug at structure instance notation 2021-07-27 11:56:33 -07:00
462.lean feat: structure instance notation with multiple sources 2021-08-12 06:18:47 -07:00
463.lean feat: structure instance notation with multiple sources 2021-08-12 06:18:47 -07:00
470_lean3.lean
471.lean fix: fixes #471 2021-05-22 15:42:52 -07:00
474_lean3.lean
481.lean fix: fixes #481 2021-05-21 20:40:26 -07:00
482.lean fix: fixes #482 2021-05-21 19:20:24 -07:00
492.lean fix: exact and refine succeed if they produce no new metavariables 2021-07-27 18:30:14 -07:00
492_lean3.lean
498.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
500_lean3.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
501.lean feat: add equality proof for named patterns 2022-01-18 12:43:01 -08:00
509.lean feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 2021-06-11 11:23:19 -07:00
536.lean chore: fix tests 2022-01-15 12:18:09 -08:00
561.lean fix: make sure isDefEqOffset does not expose kernel nat literals 2021-08-02 11:27:00 -07:00
569.lean fix: add workaround to prevent code explosion at deriving for FromJson 2021-08-05 06:58:07 -07:00
602.lean fix: fixes #602 2021-08-05 16:14:04 -07:00
616.lean fix: fixes #616 2021-08-07 07:29:54 -07:00
633.lean feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 2022-03-08 17:56:34 -08:00
644.lean feat: use contradiction at leaves 2021-08-22 18:41:02 -07:00
646.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
654.lean feat: optimized deriving DecidableEq for enumeration types 2021-09-08 16:21:32 -07:00
664.lean fix: fixes #664 2021-09-12 19:54:45 -07:00
677.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
696.lean feat: improve letIdLhs parser 2021-09-28 18:10:25 -07:00
716.lean fix: make sure Quot primitives stay in eta expanded form 2021-10-08 09:36:06 -07:00
753.lean fix: where structure instance parser 2021-12-12 07:52:52 -08:00
760.lean fix: propositions should never be considered enum types 2021-11-04 15:27:15 -07:00
764.lean feat: use binrel_no_prop% to define == notation 2021-11-09 07:46:10 -08:00
783.lean fix: use withSynthesize at elabStructInstance 2021-11-15 16:45:26 -08:00
788.lean fix: nontermination at simp [OfNat.ofNat] 2021-12-10 12:29:33 -08:00
790.lean fix: transparency settings at simp TC check 2021-11-15 18:09:31 -08:00
793.lean fix: fixes #793 2021-11-22 13:28:08 -08:00
796.lean fix: missing universe assignments made during TC resolution 2021-12-12 07:07:13 -08:00
815.lean feat: add Tomas Skrivan's TC resolution improvement 2021-12-06 17:46:11 -08:00
821.lean fix: this must be a keyword 2021-11-29 10:06:15 -08:00
837.lean fix: give preference to non-indices at findRecArg 2021-12-01 16:45:19 -08:00
847.lean feat: add support for guessing (very) simple WF relations 2022-03-02 11:52:00 -08:00
854.lean fix: auxiliary matcher definitions should be treated as abbreviations 2021-12-07 16:43:20 -08:00
860.lean chore: use termination_by' 2022-01-11 15:00:53 -08:00
879.lean fix: add missing [reducible] annotations Init/WF.lean 2022-01-12 17:12:55 -08:00
891.lean fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible 2021-12-18 10:55:42 -08:00
909.lean fix: constant folding after erasure 2022-01-03 10:33:07 -08:00
945.lean fix: equality theorem generation when named patterns are used 2022-01-18 14:37:51 -08:00
946.lean chore: remove problematic instance hasOfNatOfCoe 2022-01-20 14:47:25 -08:00
955.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
968.lean fix: use an AC-compatible ordering on Expr at simp 2022-01-22 09:42:59 -08:00
972.lean fix: igore instance implicit arguments in term ordering used at simp 2022-01-24 18:57:31 -08:00
983.lean fix: induction MetaM tactic 2022-01-31 13:41:38 -08:00
986.lean fix: splitMatch tactic 2022-02-02 15:06:03 -08:00
988.lean feat: use mkCongrSimp? at simp 2022-02-07 16:45:01 -08:00
998.lean fix: avoid unnecessary matcheApp.addArgs at BRecOn and Fix 2022-02-08 15:06:14 -08:00
998Export.lean fix: avoid unnecessary matcheApp.addArgs at BRecOn and Fix 2022-02-08 15:06:14 -08:00
1016.lean fix: mark auxiliary noConfusion declarations for enumeration types as [reducible] 2022-02-14 12:03:49 -08:00
1017.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
1018.lean feat: (generalizing := true) is the default behavior for match-expressions 2022-02-15 11:12:04 -08:00
1020.lean fix: mkLetRecClosureFor for nested let-recs 2022-02-16 12:44:02 -08:00
1022.lean feat: support for acyclicity at unifyEqs 2022-02-27 10:03:40 -08:00
1024.lean fix: when performing contextual simplification, and arrow may become a dependent arrow 2022-02-23 18:43:32 -08:00
1025.lean fix: remove [..] annotation from if simp theorems 2022-02-23 16:28:12 -08:00
1029.lean fix: substEqs may close input goal 2022-02-25 08:07:23 -08:00
1030.lean fix: add workarounds to code generator 2022-02-25 08:47:56 -08:00
1037.lean fix: use withoutErrToSorry at apply 2022-03-04 14:36:10 -08:00
1385.lean chore: rename PointedType => NonemptyType 2022-01-15 11:43:53 -08:00
1954.lean
1968.lean
ac_expr.lean feat: rename tactic byCases => by_cases 2022-02-10 17:11:07 -08:00
ack.lean test: add test for #879 2022-01-12 16:25:09 -08:00
ACltBug.lean fix: missing condition at lpo case 3 2022-01-28 09:47:35 -08:00
alg.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
allGoals.lean chore: fix tests 2021-09-16 10:29:38 -07:00
anonymous_ctor_error_msg.lean
anonymousCtor.lean
applytransp.lean
approxDepth.lean feat: make sure Expr.approxDepth does not overflow 2022-01-22 07:45:19 -08:00
array1.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
assertAfterBug.lean
autoboundIssues.lean feat: refine auto bound implicit locals 2021-03-23 17:33:15 -07:00
autoLift.lean
autoLiftIssue.lean
autoparam.lean
backtrackable_estate.lean
balg.lean chore: fix tests 2022-01-20 15:25:59 -08:00
bigctor.lean chore: disable injectivity theorems generation for big structure tests 2021-05-15 21:30:40 -07:00
bigmul.lean
bigop.lean chore: fix tests 2021-08-07 13:22:58 -07:00
binderNotation.lean
binrel.lean chore: fixes tests 2021-04-22 20:22:43 -07:00
binrelmacros.lean feat: use binrel! gadget to define >, <, ... notations 2020-12-29 16:53:10 -08:00
borrowBug.lean
bubble.lean fix: recursive applications in discriminants 2022-01-13 09:56:33 -08:00
byteSliceIssue.lean test: add missing test for issue #998 2022-02-09 18:02:01 -08:00
calc.lean chore: fix calc test 2021-08-25 06:59:46 -07:00
calcBug.lean fix: use show .. from .. to implement calc 2021-08-29 11:33:50 -07:00
casesUsing.lean chore: fix tests 2021-08-07 13:22:58 -07:00
catchThe.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
cdotTests.lean
check.lean
check_failure.lean fix: #check_failure command should succeed if there are stuck TC problems 2021-11-15 16:56:55 -08:00
checkAssignmentIssue.lean
choiceExpectedTypeBug.lean
choiceMacroRules.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
class_inductive.lean
classAbbrev.lean feat: class abbrev now supports a type spec (+ test) 2021-05-20 15:23:30 -07:00
closure1.lean chore: fix tests 2021-09-07 19:14:30 -07:00
coeIssue1.lean
coeIssue2.lean chore: fix tests 2022-01-20 15:25:59 -08:00
coeIssue3.lean chore: fix tests 2022-01-20 15:25:59 -08:00
coeIssues4.lean chore: remove problematic instance hasOfNatOfCoe 2022-01-20 14:47:25 -08:00
coelambda.lean
CoeNew.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
coeSort1.lean chore: fix tests 2022-01-20 15:25:59 -08:00
coeSort2.lean
combinatorsAndWF.lean test: plan for supporting combinators (e.g., List.foldl) in WF recursion 2022-03-02 15:18:25 -08:00
CommandExtOverlap.lean feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
compiler_erase_bug.lean fix: do not infer type in erase_irrelevant 2022-01-03 07:13:55 -08:00
compiler_proj_bug.lean
concatElim.lean chore: fix test 2021-08-21 15:07:36 -07:00
congrThm.lean feat: add mkCongrSimp.mkProof 2022-02-04 17:57:28 -08:00
constantCompilerBug.lean
constFun.lean
constFun2.lean
contra.lean
contradiction1.lean feat: contradiction catches empty inductive types 2021-03-21 21:48:43 -07:00
contradictionExfalso.lean feat: use exfalso at ElimEmptyInductive 2021-08-22 18:16:14 -07:00
contradictionLoop.lean fix: deep recursion at contradiction 2021-08-17 21:32:32 -07:00
conv1.lean chore: fix tests 2021-09-16 10:29:38 -07:00
core.lean
crashDiv0.lean
csimp_type_error.lean
ctorAutoParams.lean feat: while and repeat macros 2022-02-24 16:26:07 -08:00
Daniel1.lean
decAuxBug.lean fix: bug at decAux? 2021-09-20 07:12:57 -07:00
decClassical.lean chore: fix tests 2021-08-07 13:22:58 -07:00
decEq.lean
decidelet.lean
decreasingTacticUpdatedEnvIssue.lean fix: unfold auxiliary theorems created by decreasing_tactic 2022-02-23 09:02:23 -08:00
deep1.lean refactor: remove Monad Option and Alternative Option 2021-03-20 18:25:25 -07:00
def1.lean
def2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
def3.lean
def4.lean test: split tactic tests 2021-08-31 17:09:00 -07:00
def5.lean
def6.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def7.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
def8.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
def9.lean test: add "discriminant refinement" tests 2021-03-24 19:10:50 -07:00
def10.lean test: split tactic tests 2021-08-31 17:09:00 -07:00
def11.lean
def12.lean chore: fix tests 2022-01-15 12:18:09 -08:00
def13.lean chore: fix tests 2021-08-07 13:22:58 -07:00
def14.lean
def15.lean
def16.lean
def17.lean
def18.lean
def19.lean
def20.lean test: split tactic tests 2021-08-31 17:09:00 -07:00
DefEqAssignBug.lean
depElim1.lean feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 2022-03-08 17:56:34 -08:00
depHd.lean
deriv.lean
derivingBEq.lean
derivingHashable.lean fix: Use UInt64 in deriving handler for Hashable. 2021-06-03 06:38:44 -07:00
derivingInhabited.lean
derivingRpcEncoding.lean fix: deriving RpcEncoding 2021-08-01 09:58:44 +02:00
diamond1.lean feat: register instance/reducible attribute for structuer diamond coercions 2021-08-10 07:16:59 -07:00
diamond2.lean feat: improve copyNewFieldsFrom 2021-08-10 09:08:35 -07:00
diamond3.lean fix: reduce projections of expanded structures at copyDefaultValue? 2021-08-10 20:50:59 -07:00
diamond4.lean test: default value set at copied structure 2021-08-10 19:00:34 -07:00
diamond5.lean fix: structure command diamond support 2021-08-19 07:45:21 -07:00
discrRefinement.lean feat: "discriminant refinement" for match-expressions 2021-03-23 20:40:07 -07:00
discrRefinement2.lean chore: remove ≅ notation for HEq 2021-09-15 08:06:32 -07:00
discrRefinement3.lean chore: fix tests 2022-03-03 18:13:34 -08:00
discrTreeOffset.lean feat: add support for offset terms at DiscrTree 2021-03-14 08:23:44 -07:00
discrTreeSimp.lean fix: remove @[reducible] annotation from Function.comp and Function.const 2021-11-23 07:29:25 -08:00
do_eqv.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
do_eqv_proofs.lean
doElemAsTermNotation.lean
dofun_prec.lean
doLetElse.lean feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
dollarProjIssue.lean
doNotation1.lean feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
doNotation2.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
doNotation3.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
doNotation4.lean
doNotation5.lean
doNotation6.lean
Dorais1.lean
dotNotationRecDecl.lean feat: do not consider dot notation when isAuxDecl is true 2021-08-21 16:35:32 -07:00
doTrailingAtEOI.lean
eagerInliningIssue.lean
elab_cmd.lean chore: fix tests 2021-09-16 10:29:38 -07:00
elabCmd.lean
elabIte.lean
elseCaseArrow.lean
elseIfConfusion.lean
emptycOverloadIssues.lean
enumDecEq.lean test: deriving DecidableEq for enum types 2021-09-09 17:47:23 -07:00
eqnsAtSimp.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
eqnsAtSimp2.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
eqnsAtSimp3.lean feat: add better support for discharging equation theorem hypotheses 2022-01-06 14:42:23 -08:00
eqTheoremForVec.lean fix: use default reducibility when proving equation theorems for definition 2022-01-20 08:23:51 -08:00
eqThm.lean chore: fix tests 2021-09-16 10:29:38 -07:00
etaFirst.lean
etaStruct.lean feat: eta struct support for unit-like datatypes 2021-11-26 08:36:25 -08:00
etaStructProofIrrelIssue.lean fix: eta struct and proof irrelevance issue 2021-11-27 07:15:57 -08:00
eval_unboxed_const.lean
evalBuiltinInit.lean
evalconst.lean
evalInit.lean feat: allow interpretation of constants initialized by native code 2022-03-07 10:59:49 +01:00
evalProp.lean feat: allow (decidable) propositions at #eval 2021-08-27 15:06:48 -07:00
exp.lean feat: nary generalize tactic 2021-08-30 16:31:39 -07:00
expandAbbrevAtIsClass.lean
expectedTypePropagation.lean
explicitMotive.lean
explictOpenDeclIssue.lean fix: issue raised by Andrew 2021-04-12 10:51:44 -07:00
expr1.lean chore: fix tests 2021-09-07 19:14:30 -07:00
expr_maps.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
extern.lean
extmacro.lean feat: add trivial extensible (macro) tactic 2021-03-24 09:50:56 -07:00
falseElimAtSimpLocalDecl.lean feat: use False.elim when simplifying local declarations that rewrite to False 2021-03-17 15:30:54 -07:00
fieldAbbrevInPat.lean feat: add macro for expanding field abbrev notation 2021-08-11 16:02:50 -07:00
fieldAutoBound.lean
fieldDefaultValueWithoutType.lean
fieldIssue.lean
finally.lean
finLit.lean feat: ignore nested proofs in patterns 2021-09-05 15:46:03 -07:00
finMatch.lean test: Fin match test that relies heavily on contradiction 2021-09-21 12:57:08 -07:00
flat_expr.lean
float1.lean
float_cases_bug.lean
float_from_bignum.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
floatarray.lean
foldConsts.lean
forBodyResultTypeIssue.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
forInPArray.lean
forInUniv.lean feat: in pure code, do use assume Id monad at do notation 2021-12-10 12:55:14 -08:00
forParallel.lean
french_quote.lean
fun.lean chore: fix tests 2022-01-15 12:18:09 -08:00
funext.lean
funMatchIssue.lean fix: issue at expandMatchAlts 2021-03-30 12:55:59 -07:00
generalize.lean
generalizeMany.lean feat: add Fin.succ 2022-03-05 17:36:38 -08:00
generalizeTelescope.lean
genindices.lean
getline_crash.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
haveDestruct.lean feat: have ... := ... syntax closer to let 2021-05-06 15:38:57 -07:00
hcongr.lean feat: heterogeneous congruence theorems 2021-09-14 17:23:12 -07:00
hmul2.lean
hmulDefaultIntance.lean
ifcongr.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
ifThenElseIssue.lean
ifThenElseIssue2.lean fix: add withFreshMacroScope at expandMacroImpl? 2021-10-02 16:57:25 -07:00
impByNameResolution.lean
impLambdaTac.lean chore: remove old notation 2021-10-02 15:06:40 -07:00
implicitApplyIssue.lean fix: bug at decAux? 2021-09-20 07:12:57 -07:00
implicitTypesRecCoe.lean
inaccessibleAnnotDefEqIssue.lean fix: inaccessible annotations at isDefEq issue 2021-10-27 09:26:12 -07:00
incmd.lean
ind_cmd_bug.lean
ind_whnf.lean feat: use forallTelescopeReducing 2021-10-25 13:05:23 -07:00
ind_whnf2.lean feat: missing whnf at checkParamsAndResultType 2021-10-25 13:08:43 -07:00
induction1.lean chore: fix tests 2021-09-16 10:29:38 -07:00
inductionAltExplicit.lean chore: fix mkForbiddenSet 2021-03-27 14:59:05 -07:00
inductionParse.lean fix: induction generalizing precedence 2022-01-07 10:45:45 +01:00
inductionTacticBug.lean
inductive1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
inductive2.lean
inductive_pred.lean feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 2022-03-08 17:56:34 -08:00
inductiveIndicesIssue.lean fix: improve inductive indices elaboration 2022-03-08 17:48:46 -08:00
infixprio.lean
inj1.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
inj2.lean fix: check number of explicit variables at induction/cases alternatives when @ is not used 2021-09-29 07:39:38 -07:00
injectionBug.lean
injections1.lean test: missing tests 2021-09-08 08:00:36 -07:00
injectionsIssue.lean feat: add support for HEq at injections tactic 2022-02-23 17:31:17 -08:00
injective.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
injHEq.lean feat: support for HEq at injection 2022-02-22 17:24:11 -08:00
injIssue.lean
injSimp.lean feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
inline_fn.lean
inlineLoop.lean
inliner_loop.lean
instanceIssues.lean fix: use a def-eq aware mapping at toLinearExpr 2022-02-28 13:46:36 -08:00
instances.lean
instanceWhere.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
instPatVar.lean fix: declare local instaces occurring in patterns 2022-02-12 12:01:08 -08:00
instprio.lean
instuniv.lean
int_to_nat_bug.lean
interp.lean test: remove workaround 2022-03-06 13:58:42 -08:00
intromacro.lean
IO_test.lean fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
ioRandomBytes.lean feat: IO.getRandomBytes 2021-07-24 10:45:28 +02:00
irCompilerBug.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
irreducibleIssue.lean fix: make sure irreducible constants are not unfolded when using the default reducibility setting 2022-01-26 11:55:21 -08:00
isDefEqCheckAssignmentBug.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
isDefEqConstApproxIssue.lean feat: improve "constant approximation" heuristic used at isDefEq 2022-02-19 08:09:31 -08:00
isDefEqIssue.lean
isDefEqMVarSelfIssue.lean
jason1.lean
kernel1.lean
kernel2.lean
kevin.lean
krivine.lean test: add WF test that exposes the need for better error messages 2022-03-02 12:47:19 -08:00
KyleAlg.lean feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
KyleAlgAbbrev.lean feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
lazylistThunk.lean feat: add support for guessing (very) simple WF relations 2022-03-02 11:52:00 -08:00
lean3_zulip_issues_1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
lemma.lean feat: parser alias for 'declVal' 2021-04-12 16:59:54 -07:00
letMVar.lean feat: elaborate let_mvar% 2021-10-02 16:12:50 -07:00
letrecInProofs.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
letrecWFIssue.lean test: mutual block not needed 2022-02-11 16:22:13 +01:00
level.lean
levelNamesInTacticMode.lean fix: store levelNames in the SavedContext 2022-02-24 17:47:26 -08:00
liftMethodInMacrosIssue.lean
LiftMethodIssue.lean
linearByRefl.lean feat: add src/Init/Data/Nat/Linear.lean 2022-02-24 13:45:17 -08:00
listDecEq.lean
localNameResolutionWithProj.lean
localParsers.lean
macro.lean chore: fix tests 2022-03-03 18:13:34 -08:00
macro2.lean
macro3.lean
macro_macro.lean
macroid.lean
macroParams.lean feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
manyAritySyntax.lean feat: add enum command for declaring enumeration types 2021-09-05 16:58:49 -07:00
mapTR.lean test: add mapTR test 2021-08-22 16:51:38 -07:00
match1.lean test: notation for providing names to equality proofs in match expressions is not whitespace sensitivity anymore 2022-02-14 15:51:23 -08:00
match_unit.lean
matchArrayLit.lean chore: fix tests 2021-08-07 13:22:58 -07:00
matchDiscrType.lean
matchEqs.lean feat: add simpMatch and use it at splitMatch 2021-08-31 12:53:41 -07:00
matchEqsBug.lean fix: use private names for theorems that are created on demand 2022-02-07 13:16:22 -08:00
matcherElimUniv.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
matchGenBug.lean chore: fix tests 2022-03-03 18:13:34 -08:00
matchGenIssue.lean fix: improve match generalizing feature 2021-04-26 19:22:03 -07:00
matchNoPostponing.lean
matchRw.lean
matchtac.lean test: notation for providing names to equality proofs in match expressions is not whitespace sensitivity anymore 2022-02-14 15:51:23 -08:00
matchUnifyBug.lean fix: missing whnf at Unify.unify 2021-03-21 22:38:46 -07:00
matchVarIssue.lean fix: simple match case 2021-03-24 11:46:55 -07:00
matchWithSearch.lean chore: remove unnecessary annotations 2021-03-23 20:42:59 -07:00
mathport18.lean test: mathport issue https://github.com/dselsam/mathport/issues/18 2021-08-15 08:11:20 -07:00
mathport_issue16.lean feat: add instance from CoeSort to CoeTail 2021-08-18 20:24:43 -07:00
matrix.lean chore: fix tests 2021-08-07 13:22:58 -07:00
maze.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
meta.lean chore: example 2021-04-12 16:56:10 -07:00
meta1.lean
meta2.lean fix: make sure isDefEqOffset does not expose kernel nat literals 2021-08-02 11:27:00 -07:00
meta3.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta4.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta5.lean chore: fix tests 2021-09-07 19:14:30 -07:00
meta6.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta7.lean feat: eta struct support for unit-like datatypes 2021-11-26 08:36:25 -08:00
methodsRetInhabited.lean chore: fix tests 2022-01-15 12:18:09 -08:00
Miller1.lean
missingDeclName.lean
mixedMacroRules.lean
mixfix.lean
mjissue.lean fix: skip value if type is computationally irrelevant 2022-02-17 10:41:16 -08:00
modAsClasses.lean
monadCache.lean
monadControl.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
monotone.lean fix: bug at decAux? 2021-09-20 07:12:57 -07:00
mulcomm.lean fix: instance + where + implicts issue 2021-04-24 20:07:35 -07:00
multiTargetCasesInductionIssue.lean chore: fix tests 2021-09-16 10:29:38 -07:00
mut_ind_wf.lean chore: move test to correct folder 2022-02-09 14:32:18 +01:00
mutualDefThms.lean test: simplify proofs 2022-03-02 13:57:43 -08:00
mutwf1.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
mutwf2.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
mutwf3.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
mutwf4.lean fix: expandTerminationByNonCore 2022-01-12 16:22:54 -08:00
namespaceIssue.lean
namespaceResolution.lean
nativeReflBackdoor.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
natlit.lean
nested_match_bug.lean
nestedDo.lean
nestedInductiveIssue.lean
nestedrec.lean
new_compiler.lean refactor: separate pp.funBinderTypes and pp.piBinderTypes 2021-08-09 16:13:40 +02:00
new_frontend2.lean
new_inductive.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
new_inductive2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
newfrontend1.lean chore: fix tests 2021-09-16 10:29:38 -07:00
newfrontend2.lean feat: modify notation for providing motive in "match" expressions 2022-02-14 15:36:14 -08:00
newfrontend3.lean chore: fix tests 2021-08-07 13:22:58 -07:00
newfrontend5.lean fix: bug at decAux? 2021-09-20 07:12:57 -07:00
nicerNestedDos.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
noindexAnnotation.lean chore: fix tests 2021-08-07 13:22:58 -07:00
noncomp.lean test: for Lean 3 nocomputable issue 2021-10-19 07:15:55 -07:00
noncomputable_bug.lean
nonrec.lean feat: elaborate nonrec modifier 2021-08-21 17:02:54 -07:00
obtain.lean
offsetIssue.lean
ofNat_class.lean feat: indentation sensitiviy for macro and elab commands 2021-10-18 17:16:09 -07:00
ofNatNormNum.lean feat: convert "orphan" kernel nat literals n into ofNat n 2021-09-08 14:58:13 -07:00
openInScopeBug.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
openTermTactic.lean
optParam.lean chore: fix tests 2022-01-15 12:18:09 -08:00
Ord.lean fix: compare fields top-down in deriving Ord 2022-01-03 07:02:13 -08:00
overAndPartialAppsAtWF.lean test: add test for issue #1013 2022-02-11 09:28:46 -08:00
overloaded.lean
overloadsAndDelayedCoercions.lean fix: interaction between overloaded notation and delayed coercions 2022-03-06 09:49:15 -08:00
panicAtCheckAssignment.lean chore: fix tests 2022-01-15 12:18:09 -08:00
parray1.lean feat: add PersistentArray.foldrM 2021-12-02 17:17:55 -08:00
parsePrelude.lean
parserAliasShadow.lean
partial1.lean
partialApp.lean
patbug.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
pendingInstBug.lean
pendingMVarIssue.lean fix: pending metavariable issue 2021-08-10 14:52:53 -07:00
PPTopDownAnalyze.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
precDSL.lean
print_cmd.lean chore: fix tests 2022-01-15 12:18:09 -08:00
printDecls.lean feat: record doc strings of builtin parsers & elaborators 2021-11-26 17:13:19 +01:00
prioDSL.lean
privateCtor.lean fix: inductive type name is not a necessarily a prefix of the constructor name in Lean 4 anymore 2021-09-14 18:52:43 -07:00
proofIrrelFVar.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
propagateExpectedType.lean refactor: [s : Setoid α] => {s : Setoid α} or (s : Setoid α) 2022-01-18 09:24:06 -08:00
prv.lean
psumAtWF.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
ptrAddr.lean
quasi_pattern_unification_approx_issue.lean
quotInd.lean test: for induction q with Quot.ind issue 2021-08-26 11:15:14 -07:00
range.lean
rational.lean
rc_tests.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
readerThe.lean
recInfo1.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
reduce1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
reduce2.lean
reduce3.lean chore: fix tests 2021-08-07 13:22:58 -07:00
reductionBug.lean fix: bug at reduceRec 2021-05-07 14:21:37 -07:00
reflectiveIndPred.lean chore: rename ProofBelow to below. 2021-04-26 20:33:21 +02:00
Reid1.lean
renameFixedPrefix.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
renameI.lean chore: fix tests 2021-09-16 10:29:38 -07:00
renaming.lean
Reparen.lean chore: fix tests 2021-08-06 14:05:00 -07:00
repeatConv.lean feat: add repeat tactic to conv mode 2021-10-06 14:05:44 -07:00
replace.lean
resolveLVal.lean
returnOptIssue.lean
revert1.lean chore: adapt syntax 2021-11-29 10:06:15 -08:00
root.lean
rw_inst_mvars.lean fix: instantiate mvars in rewrite tactic 2021-06-11 10:27:05 -07:00
sarray.lean feat: in pure code, do use assume Id monad at do notation 2021-12-10 12:55:14 -08:00
scc.lean
scopedCommandAfterOpen.lean fix: update tokenTable at withNamespace parser combinator 2021-08-23 09:41:36 -07:00
scopedParsers.lean
scopedParsers2.lean
secVarBug.lean fix: make sure the resulting array size is equal to the number of binders 2021-05-04 19:46:14 -07:00
set.lean
setOptionTermTactic.lean fix: make sure simp only still uses eq_self 2021-08-30 09:50:11 -07:00
sharecommon.lean
sigmaprec.lean
simp1.lean chore: fix test 2022-02-06 09:15:39 -08:00
simp2.lean
simp3.lean
simp4.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
simp5.lean
simp6.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
simp7.lean chore: fix tests 2022-01-15 12:18:09 -08:00
simp_all.lean feat: add simp_all tactic 2021-03-19 22:34:35 -07:00
simp_all_contextual.lean feat: contextual := true at simp_all 2021-03-24 15:49:31 -07:00
simpArith1.lean feat: simplify nested arith expressions 2022-02-27 09:01:52 -08:00
simpAtDefIssue.lean fix: registers eqns info before adding definition 2022-01-06 12:24:40 -08:00
simpBool.lean feat: improve SimpTheorem preprocessor 2022-02-28 18:27:36 -08:00
simpBug.lean fix: using incorrect local context to process simp arguments 2021-08-26 12:49:12 -07:00
simpCnstr1.lean feat: simplify nested arith expressions 2022-02-27 09:01:52 -08:00
simpCondLemma.lean
simpDefToUnfold.lean feat: allow users to mark definitions with [simp] 2021-03-17 19:11:55 -07:00
simpDischargeLoop.lean fix: missing withoutModifyingState at elabSimpConfig 2021-05-16 13:07:13 -07:00
simpExtraArgsBug.lean fix: bug at tryLemmaCore when numExtraArgs > 1 2021-10-18 13:59:19 -07:00
simpImpLocal.lean
simpInv.lean feat: elaborate <- modifier at simp arguments 2021-08-15 07:07:58 -07:00
simpIssue.lean fix: do not validate local eq theorems 2022-01-27 11:50:20 -08:00
simpLoopBug.lean fix: bug at simpLoop 2021-12-18 06:48:08 -08:00
simpMatchDiscr.lean feat: while and repeat macros 2022-02-24 16:26:07 -08:00
simpOnly.lean fix: make sure simp only still uses eq_self 2021-08-30 09:50:11 -07:00
simpPartialApp.lean fix: getMatchWithExtra 2021-09-25 08:36:12 -07:00
simpPreprocess.lean
simpPrio.lean fix: prefer simp lemmas with *higher* priority 2021-11-22 11:52:45 -08:00
simpRwBug.lean fix: missing whnf at tryLemma? 2021-08-30 08:33:58 -07:00
simpStar.lean chore: fix tests 2021-09-16 10:29:38 -07:00
simpStarHyp.lean fix: location notation and simp 2021-03-19 19:54:22 -07:00
simpUnfoldAbbrev.lean fix: unfold x<y in discrimination tree module 2021-11-23 07:34:51 -08:00
sizeof1.lean
sizeof2.lean
sizeof3.lean
sizeof4.lean feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters 2022-03-08 17:56:34 -08:00
sizeof5.lean
sizeof6.lean
smartUnfoldingBug.lean refactor: optimize critical import path 2021-12-06 08:05:24 -08:00
spec_issue.lean
specbug.lean
specialize1.lean feat: add specialize tactic 2021-09-08 08:00:02 -07:00
specialize2.lean feat: rename tactic byCases => by_cases 2022-02-10 17:11:07 -08:00
split1.lean feat: add simpMatch and use it at splitMatch 2021-08-31 12:53:41 -07:00
split2.lean fix: splitMatch tactic 2022-02-02 15:06:03 -08:00
split3.lean fix: splitMatch tactic 2022-02-02 15:06:03 -08:00
splitIssue.lean fix: auto implicit locals in inductive families 2022-03-05 15:47:20 -08:00
stateRef.lean
streamEqIssue.lean fix: heuristic for deciding which additional propositions must be included in equality theorems 2022-02-24 17:17:07 -08:00
strInterpolation.lean
strLitProj.lean fix: projection of string literals 2021-05-07 14:38:21 -07:00
struct1.lean
struct2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
struct3.lean test: add *> laziness test 2021-09-07 18:03:15 -07:00
struct_inst_typed.lean
struct_instance_in_eqn.lean
structInst.lean
structInst2.lean chore: fix some tests 2021-09-07 17:20:21 -07:00
structInst3.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
structInst4.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
structNoBody.lean
structPrivateFieldBug.lean fix: private field + default value bug 2021-08-09 19:01:08 -07:00
structPrivateFieldBug2.lean test: overriding default value of private field 2021-08-09 19:01:08 -07:00
structuralEqns.lean feat: add mkUnfoldProof 2022-01-07 13:51:45 -08:00
structuralEqns2.lean fix: do not split on if-then-else terms when generating equation theorems 2022-02-09 17:43:35 -08:00
structuralEqns3.lean feat: add mkUnfoldProof 2022-01-07 13:51:45 -08:00
structuralIssue.lean refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
structuralIssue2.lean fix: improve structural recursion 2021-04-13 10:31:43 -07:00
structuralRec1.lean fix: deal with params for inductive predicates. 2021-06-06 06:40:09 -07:00
structure.lean Feat: Add getAllParentStructures 2021-04-07 18:06:10 -07:00
stuckMVarBug.lean
stuckTC.lean fix: discrimination trees and "stuck" terms 2022-03-05 15:12:20 -08:00
stxKindInsideNamespace.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
stxMacro.lean
subst.lean chore: fix tests 2021-08-07 13:22:58 -07:00
subst1.lean
subtype_inj.lean
suffices.lean
syntax1.lean
syntaxAbbrevQuot.lean feat: support syntax abbreviations in dynamic quotations 2021-12-15 11:17:58 +00:00
syntaxPrio.lean
synth1.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
synthPending1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
synthPendingBug.lean fix: synthPending bug 2021-08-04 20:07:06 -07:00
tactic.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
tactic1.lean chore: add sorry tactic 2021-09-08 08:10:37 -07:00
tacticExtOverlap.lean feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
tacticTests.lean fix: induction/cases: accept wildcard alternative even if some (but not all) cases have been excluded 2021-05-06 14:28:00 +02:00
takeSimpEqns.lean fix: use simpTargetStar when proving equation theorems for recursive definitions 2022-02-08 11:43:45 -08:00
task_test.lean
task_test2.lean
task_test_io.lean
tcUnivIssue.lean fix: TC issue introduced by recent bug fix 2021-08-23 17:32:19 -07:00
termElab.lean feat: heterogeneous Append experiment 2020-12-01 16:32:41 -08:00
termParserAttr.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
TermSeq.lean fix: improve widening operator used at the ElimDeadBranches abstract interpreter 2021-10-06 12:54:07 -07:00
test_single.sh
toExpr.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
toFromJson.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
trace.lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
traceElabIssue.lean fix: tolerate type incorrect terms 2021-04-29 21:34:15 -07:00
trans.lean chore: fix test 2021-08-25 07:00:25 -07:00
tryHeuristicPerfIssue.lean feat: add basic isDefEq cache 2021-07-28 16:29:44 -07:00
tryHeuristicPerfIssue2.lean feat: add basic isDefEq cache 2021-07-28 16:29:44 -07:00
tryPostponeIssue.lean fix: improve tryPostponeIfMVar 2022-02-03 13:24:19 -08:00
type_class_performance1.lean
typeAscImp.lean feat: type ascription should disable implicit lambdas 2021-05-12 19:29:36 -07:00
typeclass_append.lean
typeclass_coerce.lean chore: increase threshold for Windows workaround in the previous commit 2021-05-15 21:15:37 -07:00
typeclass_diamond.lean chore: increase threshold for Windows workaround in the previous commit 2021-05-15 21:15:37 -07:00
typeclass_easy.lean
typeclass_loop.lean
typeclass_metas_internal_goals1.lean
typeclass_metas_internal_goals2.lean
typeclass_metas_internal_goals3.lean
typeclass_metas_internal_goals4.lean
typeclass_outparam.lean
ubscalar.lean
unexpected_result_with_bind.lean
unfoldr.lean test: use notation 2022-03-06 19:28:01 -08:00
unif_issue.lean
unif_issue2.lean
unifhint1.lean
unifhint2.lean
unifhint3.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
unihint.lean
univIssue.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
update.lean
utf8英語.lean fix: UTF-8 file path support for lean on Windows 2021-09-22 12:21:52 +02:00
wfEqns1.lean fix: use PSum instead of Sum when using well-founded recursion 2022-02-17 16:14:34 -08:00
wfEqns2.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
wfEqns3.lean chore: use termination_by' 2022-01-11 15:00:53 -08:00
wfEqns4.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
wfEqnsIssue.lean fix: invalid rewrite when proving equation theorems for declaration using well-founded recursion 2022-02-22 16:38:51 -08:00
wfForIn.lean feat: elaborate for h : x in xs do ... notation 2022-03-03 19:52:26 -08:00
wfOverapplicationIssue.lean fix: recursive overapplication at WF/Fix.lean 2022-03-03 18:13:34 -08:00
wfrecUnary.lean chore: use termination_by' 2022-01-11 15:00:53 -08:00
WFRelSearch.lean feat: add getForbiddenByTrivialSizeOf 2022-03-03 11:12:32 -08:00
wfSum.lean feat: isolate fixed prefix at well-founded recursion 2022-02-18 10:40:32 -08:00
where1.lean
whileRepeat.lean feat: while and repeat macros 2022-02-24 16:26:07 -08:00
whnfDelayedMVarIssue.lean
WindowsNewlines.lean
withReducibleAndInstancesCrash.lean