max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean
History
Leonardo de Moura 193d4dc9f5 feat: optimized deriving DecidableEq for enumeration types 
The proof term is liner on the number of constructors, but type
checking is not linear because the reduction engine in the kernel is
not efficient.
2021-09-08 16:21:32 -07:00
..
interactive feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
Reformat chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
run feat: optimized deriving DecidableEq for enumeration types 2021-09-08 16:21:32 -07:00
server chore: fix tests 2021-08-24 08:57:41 -07:00
trust0
.gitignore
217.lean
217.lean.expected.out
220.lean
220.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
223.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
223.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
236.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
236.lean.expected.out feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
241.lean fix: fixes #241 2021-05-22 19:10:07 -07:00
241.lean.expected.out fix: fixes #241 2021-05-22 19:10:07 -07:00
242.lean fix: fixes #242 2021-08-06 18:39:55 -07:00
242.lean.expected.out fix: fixes #242 2021-08-06 18:39:55 -07:00
243.lean fix: fixes #243 2021-05-03 13:01:16 -07:00
243.lean.expected.out feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
247.lean fix: fixes #247 2021-04-15 12:33:45 -07:00
247.lean.expected.out fix: no method lift over let 2021-04-24 19:33:55 -07:00
248.lean fix: fixes #248 2021-05-03 18:20:36 -07:00
248.lean.expected.out fix: fixes #248 2021-05-03 18:20:36 -07:00
255.lean
255.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
276.lean feat: add PEmpty 2021-08-06 19:18:22 -07:00
276.lean.expected.out feat: add PEmpty 2021-08-06 19:18:22 -07:00
277a.lean feat: notation: unfold to prechecked quotation 2021-04-27 16:38:37 -07:00
277a.lean.expected.out feat: notation: unfold to prechecked quotation 2021-04-27 16:38:37 -07:00
277b.lean
277b.lean.expected.out
283.lean
283.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
297.lean
297.lean.expected.out feat: allow universes metavariables from any depth to be assigned when ignoreLevelDepth is true 2021-08-18 20:20:51 -07:00
301.lean
301.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
302.lean fix: fixes #302 2021-02-03 15:04:18 -08:00
302.lean.expected.out fix: save/restore state at elabTypeWithAutoBoundImplicit 2021-02-03 15:04:18 -08:00
307.lean test: for issues #306 and #307 2021-02-06 12:48:43 -08:00
307.lean.expected.out test: for issues #306 and #307 2021-02-06 12:48:43 -08:00
309.lean fix: make sure kernel checks examples 2021-02-25 13:34:27 -08:00
309.lean.expected.out fix: make sure kernel checks examples 2021-02-25 13:34:27 -08:00
331.lean feat: improve error message 2021-03-05 13:42:54 -08:00
331.lean.expected.out feat: improve error message 2021-03-05 13:42:54 -08:00
343.lean chore: fix tests 2021-08-13 17:24:58 -07:00
343.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
345.lean fix: fixes #345 2021-03-11 18:59:39 -08:00
345.lean.expected.out feat: allow universes metavariables from any depth to be assigned when ignoreLevelDepth is true 2021-08-18 20:20:51 -07:00
346.lean chore: improve error message 2021-03-16 20:42:38 -07:00
346.lean.expected.out chore: improve error message 2021-03-16 20:42:38 -07:00
348.lean fix: fixes #348 2021-03-16 17:50:40 -07:00
348.lean.expected.out feat: hide elaboration errors from partial syntax trees by default 2021-04-13 19:24:35 +02:00
353.lean fix: register new metavariables created when applying default instance 2021-03-16 17:31:51 -07:00
353.lean.expected.out fix: register new metavariables created when applying default instance 2021-03-16 17:31:51 -07:00
366.lean fix: fixes #366 2021-03-23 16:02:45 -07:00
366.lean.expected.out fix: TC issue introduced by recent bug fix 2021-08-23 17:32:19 -07:00
370.lean fix: fixes #370 2021-08-06 12:52:23 -07:00
370.lean.expected.out fix: fixes #370 2021-08-06 12:52:23 -07:00
386.lean fix: fixes #386 2021-04-11 20:57:39 -07:00
386.lean.expected.out fix: fixes #386 2021-04-11 20:57:39 -07:00
389.lean test: expand test for 389 2021-04-11 20:55:33 -07:00
389.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
414.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
414.lean.expected.out fix: fixes #414 2021-04-19 15:02:26 -07:00
415.lean feat: closes #415 2021-05-03 18:04:01 -07:00
415.lean.expected.out feat: pp.analyze detect when struct-inst type needed 2021-08-03 09:13:18 +02:00
421.lean fix: closes #421 2021-04-23 12:27:39 -07:00
421.lean.expected.out fix: closes #421 2021-04-23 12:27:39 -07:00
423.lean test: add second example for issue #423 2021-04-25 10:35:23 -07:00
423.lean.expected.out chore: fix tests 2021-08-13 17:24:58 -07:00
435.lean fix: fixes #435 2021-05-02 18:16:57 -07:00
435.lean.expected.out fix: avoid "failed to evaluate" error when extension has sorry 2021-05-04 20:57:53 -07:00
435b.lean fix: add basic support for accessing the field of a section variable in the notation prechecker 2021-05-04 22:41:25 -07:00
435b.lean.expected.out fix: add basic support for accessing the field of a section variable in the notation prechecker 2021-05-04 22:41:25 -07:00
439.lean feat: flag to trust coercions 2021-08-03 09:13:18 +02:00
439.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
440.lean feat: closes #440 2021-05-15 20:54:54 -07:00
440.lean.expected.out feat: closes #440 2021-05-15 20:54:54 -07:00
448.lean fix: fixes #448 2021-05-10 20:07:28 -07:00
448.lean.expected.out fix: fixes #448 2021-05-10 20:07:28 -07:00
449.lean fix: fixes #449 2021-05-10 13:10:59 -07:00
449.lean.expected.out fix: fixes #449 2021-05-10 13:10:59 -07:00
450.lean fix: fixes #450 2021-05-10 13:55:06 -07:00
450.lean.expected.out fix: fixes #450 2021-05-10 13:55:06 -07:00
456.lean fix: fixes #456 2021-05-11 21:07:21 -07:00
456.lean.expected.out fix: fixes #456 2021-05-11 21:07:21 -07:00
469.lean fix: check arity in notation unexpander 2021-07-22 16:59:19 +02:00
469.lean.expected.out fix: check arity in notation unexpander 2021-07-22 16:59:19 +02:00
474.lean feat: add Meta.abstract 2021-08-06 18:19:06 -07:00
474.lean.expected.out feat: add Meta.abstract 2021-08-06 18:19:06 -07:00
496.lean chore: improve error message when compiling code containing axioms or noncomputable definitions 2021-05-31 20:27:15 -07:00
496.lean.expected.out chore: improve error message when compiling code containing axioms or noncomputable definitions 2021-05-31 20:27:15 -07:00
529.lean feat: add withOpenDecl and withOpen parsers 2021-08-22 20:50:35 -07:00
529.lean.expected.out feat: add withOpenDecl and withOpen parsers 2021-08-22 20:50:35 -07:00
550.lean fix: offset support at isDefEq should not use HAdd.hAdd 2021-07-27 16:16:03 -07:00
550.lean.expected.out fix: offset support at isDefEq should not use HAdd.hAdd 2021-07-27 16:16:03 -07:00
586.lean fix: ensure hygiene of double-quoted names 2021-07-30 07:17:50 -07:00
586.lean.expected.out fix: ensure hygiene of double-quoted names 2021-07-30 07:17:50 -07:00
593.lean fix: fixes #593 2021-08-02 10:46:12 -07:00
593.lean.expected.out feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
603.lean feat: borrow inference: preserve mutual tail calls 2021-08-05 06:26:06 -07:00
603.lean.expected.out feat: borrow inference: preserve mutual tail calls 2021-08-05 06:26:06 -07:00
604.lean fix: fixes #604 2021-08-04 17:19:17 -07:00
604.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
620.lean fix: fixes #620 2021-08-10 15:06:06 -07:00
620.lean.expected.out fix: fixes #620 2021-08-10 15:06:06 -07:00
621.lean fix: fixes #621 2021-08-10 21:15:35 -07:00
621.lean.expected.out fix: fixes #621 2021-08-10 21:15:35 -07:00
625.lean fix: handle MData-wrapped app fns consistently in delaborator 2021-08-11 18:53:32 +02:00
625.lean.expected.out fix: handle MData-wrapped app fns consistently in delaborator 2021-08-11 18:53:32 +02:00
629.lean fix: BinomialHeap: insert (head h) (tail h) = h 2021-08-17 10:19:12 -07:00
629.lean.expected.out fix: BinomialHeap: insert (head h) (tail h) = h 2021-08-17 10:19:12 -07:00
641.lean feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
641.lean.expected.out feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
653.lean fix: fixes #653 2021-09-04 18:42:33 -07:00
653.lean.expected.out fix: fixes #653 2021-09-04 18:42:33 -07:00
655.lean fix: fixes #655 2021-09-07 12:17:28 -07:00
655.lean.expected.out fix: fixes #655 2021-09-07 12:17:28 -07:00
abst.lean chore: fix tests 2021-09-07 19:14:30 -07:00
abst.lean.expected.out
appParserIssue.lean
appParserIssue.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
attrCmd.lean
attrCmd.lean.expected.out
autobound_and_macroscopes.lean feat: notation: unfold to prechecked quotation 2021-04-27 16:38:37 -07:00
autobound_and_macroscopes.lean.expected.out
autoBoundErrorMsg.lean test: add test for former weird error message 2021-03-23 18:16:06 -07:00
autoBoundErrorMsg.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
autoBoundImplicits1.lean
autoBoundImplicits1.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
autoBoundImplicits2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
autoBoundImplicits2.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
autoBoundPostponeLoop.lean fix: nontermination 2021-03-18 14:23:03 -07:00
autoBoundPostponeLoop.lean.expected.out feat: refine auto bound implicit locals 2021-03-23 17:33:15 -07:00
autoPPExplicit.lean
autoPPExplicit.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
auxDeclIssue.lean feat: improve error handling in tactic blocks 2021-05-15 20:18:48 -07:00
auxDeclIssue.lean.expected.out feat: improve error handling in tactic blocks 2021-05-15 20:18:48 -07:00
badBinderName.lean
badBinderName.lean.expected.out
badIhName.lean refactor: use Lean version 2021-05-03 10:06:20 -07:00
badIhName.lean.expected.out refactor: use Lean version 2021-05-03 10:06:20 -07:00
beginEndAsMacro.lean feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
beginEndAsMacro.lean.expected.out chore: fix tests 2021-05-17 15:09:51 -07:00
bigUnivOffsets.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
bigUnivOffsets.lean.expected.out feat: add option maxUniverseOffset 2021-02-04 17:17:51 -08:00
binderCacheIssue.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
binderCacheIssue.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
binderCacheIssue2.lean fix: take binder information into account when caching results 2021-05-03 21:02:23 -07:00
binderCacheIssue2.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
binomialHeap.lean chore: add test case for BinomialHeap 2021-08-17 10:19:12 -07:00
binomialHeap.lean.expected.out chore: add test case for BinomialHeap 2021-08-17 10:19:12 -07:00
binop_lazy.lean test: use <|> at binop_lazy test 2021-09-07 17:10:36 -07:00
binop_lazy.lean.expected.out feat: elaborate binop_lazy% 2021-09-07 13:30:09 -07:00
binopIssues.lean feat: new elaborator for binop% 2021-08-13 15:44:59 -07:00
binopIssues.lean.expected.out feat: new elaborator for binop% 2021-08-13 15:44:59 -07:00
binsearch.lean
binsearch.lean.expected.out
bitwise.lean fix: bitwise shift overflow of UInt types 2021-03-17 10:08:02 +01:00
bitwise.lean.expected.out fix: bitwise shift overflow of UInt types 2021-03-17 10:08:02 +01:00
byCasesMetaM.lean feat: add Meta.byCases helper tactic 2021-08-16 14:58:51 -07:00
byCasesMetaM.lean.expected.out feat: add Meta.byCases helper tactic 2021-08-16 14:58:51 -07:00
bytearray.lean feat: add UInt64 unpackings 2021-07-24 10:45:28 +02:00
bytearray.lean.expected.out feat: add UInt64 unpackings 2021-07-24 10:45:28 +02:00
cacheIssue.lean fix: cache issue at instantiateBetaRevRange 2021-05-02 17:00:35 -07:00
cacheIssue.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
calcErrors.lean feat: elaborator for the calc notation 2021-08-31 09:56:49 -07:00
calcErrors.lean.expected.out chore: add type to error message 2021-08-31 10:06:22 -07:00
cdotAtSimpArg.lean feat: allow cdot notation at simp 2021-04-09 19:50:42 -07:00
cdotAtSimpArg.lean.expected.out feat: allow cdot notation at simp 2021-04-09 19:50:42 -07:00
cdotTuple.lean
cdotTuple.lean.expected.out
class_def_must_fail.lean
class_def_must_fail.lean.expected.out
classBadOutParam.lean
classBadOutParam.lean.expected.out
collectDepsIssue.lean
collectDepsIssue.lean.expected.out
commandPrefix.lean feat: introduce arg precedence 2021-03-22 16:33:37 +01:00
commandPrefix.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
constDelab.lean fix: Delaborator for constants 2021-03-12 19:51:27 -08:00
constDelab.lean.expected.out fix: Delaborator for constants 2021-03-12 19:51:27 -08:00
constructorTac.lean feat: add constructor tactic 2021-05-06 10:40:56 -07:00
constructorTac.lean.expected.out feat: add constructor tactic 2021-05-06 10:40:56 -07:00
conv1.lean feat: change lhs and rhs conv tactic semantics 2021-09-05 09:29:40 -07:00
conv1.lean.expected.out feat: change lhs and rhs conv tactic semantics 2021-09-05 09:29:40 -07:00
copy-produced
csimpAttr.lean feat: apply csimp attribute constant replacements 2021-08-21 12:22:15 -07:00
csimpAttr.lean.expected.out feat: apply csimp attribute constant replacements 2021-08-21 12:22:15 -07:00
csimpAttrAppend.lean feat: use simple List.append definition and add csimp theorem 2021-08-21 16:11:54 -07:00
csimpAttrAppend.lean.expected.out feat: use simple List.append definition and add csimp theorem 2021-08-21 16:11:54 -07:00
ctor_layout.lean
ctor_layout.lean.expected.out
dbgMacros.lean chore: fix tests 2021-03-11 11:35:51 -08:00
dbgMacros.lean.expected.out chore: fix tests 2021-03-11 11:35:51 -08:00
decimals.lean
decimals.lean.expected.out
defaultInstance.lean
defaultInstance.lean.expected.out chore: improve error message 2021-02-05 12:26:39 -08:00
defInst.lean feat: add support for classes with a prefix of outParams at deriving ... 2021-09-03 11:33:09 -07:00
defInst.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
delabUnexpand.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
delabUnexpand.lean.expected.out feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
derivingRepr.lean test: use decide and nativeDecide 2021-03-11 07:46:33 -08:00
derivingRepr.lean.expected.out fix: fix deriving Repr for structure-like inductives 2021-02-25 13:38:33 -08:00
diamond1.lean feat: structure diamonds basic support 2021-08-09 19:01:08 -07:00
diamond1.lean.expected.out feat: structure diamonds basic support 2021-08-09 19:01:08 -07:00
diamond2.lean feat: add coercion to parent structure whose fields having been copied 2021-08-09 19:01:08 -07:00
diamond2.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
diamond3.lean test: structure diamond coercion 2021-08-10 06:31:44 -07:00
diamond3.lean.expected.out fix: binder annotation for class diamond coercions 2021-08-10 06:59:28 -07:00
diamond4.lean fix: binder annotation for class diamond coercions 2021-08-10 06:59:28 -07:00
diamond4.lean.expected.out fix: binder annotation for class diamond coercions 2021-08-10 06:59:28 -07:00
diamond5.lean fix: generation of to* field names 2021-08-11 17:25:02 -07:00
diamond5.lean.expected.out fix: generation of to* field names 2021-08-11 17:25:02 -07:00
diamond6.lean test: copyNewFieldsFrom 2021-08-10 09:19:27 -07:00
diamond6.lean.expected.out test: copyNewFieldsFrom 2021-08-10 09:19:27 -07:00
diamond7.lean test: add classes up to Field 2021-08-11 08:51:49 -07:00
diamond7.lean.expected.out test: add classes up to Field 2021-08-11 08:51:49 -07:00
docStr.lean chore: remove volatile cases from test 2021-03-17 12:32:25 +01:00
docStr.lean.expected.out chore: remove volatile cases from test 2021-03-17 12:32:25 +01:00
doErrorMsg.lean
doErrorMsg.lean.expected.out refactor: remove explicitly lifted IO functions and move more things into IO.FS 2021-06-11 17:53:51 -07:00
doIfLet.lean
doIfLet.lean.expected.out
doIssue.lean
doIssue.lean.expected.out fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
doLetLoop.lean fix: ensure ill-formed if do-statements do not trigger non termination 2021-04-13 15:51:20 -07:00
doLetLoop.lean.expected.out fix: ensure ill-formed if do-statements do not trigger non termination 2021-04-13 15:51:20 -07:00
doNotation1.lean
doNotation1.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
doSeqRightIssue.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
doSeqRightIssue.lean.expected.out
eagerCoeExpansion.lean feat: eager coe expansion 2021-02-14 11:34:08 -08:00
eagerCoeExpansion.lean.expected.out chore: "fix" <|> notation declaration 2021-09-07 17:29:27 -07:00
eagerUnfoldingIssue.lean fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
eagerUnfoldingIssue.lean.expected.out fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
elseifDoErrorPos.lean
elseifDoErrorPos.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
emptyc.lean
emptyc.lean.expected.out feat: pp.analyze detect when struct-inst type needed 2021-08-03 09:13:18 +02:00
eoi.lean chore: improve EOI error message 2021-04-03 11:56:26 +02:00
eoi.lean.expected.out feat: hide elaboration errors from partial syntax trees by default 2021-04-13 19:24:35 +02:00
eraseInsts.lean feat: allow instances to be (temporarily) erased 2021-08-31 15:30:29 -07:00
eraseInsts.lean.expected.out feat: allow instances to be (temporarily) erased 2021-08-31 15:30:29 -07:00
eraseSimp.lean feat: simp [-decl] 2021-03-04 17:50:44 -08:00
eraseSimp.lean.expected.out feat: allow user to "erase" [simp] lemmas 2021-03-04 11:36:12 -08:00
errorRecoveryBug.lean fix: antipattern 2021-04-07 10:26:05 -07:00
errorRecoveryBug.lean.expected.out fix: antipattern 2021-04-07 10:26:05 -07:00
eta.lean feat: add Expr.eta 2021-04-09 14:21:21 -07:00
eta.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
eval_except.lean
eval_except.lean.expected.out
evalSorry.lean
evalSorry.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
evalWithMVar.lean
evalWithMVar.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
exactErrorPos.lean feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
exactErrorPos.lean.expected.out feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
exitAfterParseError.lean
exitAfterParseError.lean.expected.out feat: hide elaboration errors from partial syntax trees by default 2021-04-13 19:24:35 +02:00
extract.lean
extract.lean.expected.out
file_not_found.lean feat: make FilePath a concrete type 2021-05-28 14:19:59 +02:00
file_not_found.lean.expected.out
filePath.lean feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
filePath.lean.expected.out feat: make FilePath a concrete type 2021-05-28 14:19:59 +02:00
forallMetaBounded.lean fix: forallMetaTelescope issue 2021-08-06 09:47:10 -07:00
forallMetaBounded.lean.expected.out fix: forallMetaTelescope issue 2021-08-06 09:47:10 -07:00
forErrors.lean
forErrors.lean.expected.out
Format.lean
Format.lean.expected.out
funExpected.lean
funExpected.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
funInfoBug.lean
funInfoBug.lean.expected.out
gcd.lean feat: add Nat.gcd 2021-03-07 18:47:02 -08:00
gcd.lean.expected.out feat: add Nat.gcd 2021-03-07 18:47:02 -08:00
have.lean feat: have: remove unnecessary whitespace check and allow name- and type-less have 2021-05-25 14:25:14 +02:00
have.lean.expected.out feat: have ... := ... syntax closer to let 2021-05-06 15:38:57 -07:00
hidingInaccessibleNames.lean chore: two comments about bad pp.analyze behavior 2021-08-03 09:13:18 +02:00
hidingInaccessibleNames.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
holeErrors.lean
holeErrors.lean.expected.out fix: mkAtomFrom: generate synthetic position like other *From functions 2021-07-19 13:24:59 -07:00
holes.lean
holes.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
hygienicIntro.lean feat: add tactic macro unhygienic <tactic-seq> 2021-04-10 16:18:40 -07:00
hygienicIntro.lean.expected.out feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
implicitLambdaIssue.lean chore: fixes tests 2021-04-22 20:22:43 -07:00
implicitLambdaIssue.lean.expected.out test: add Kevin and Yakov's examples 2021-03-25 17:22:14 -07:00
implicitTypePos.lean fix: position information for implicit type 2021-08-26 08:07:16 -07:00
implicitTypePos.lean.expected.out fix: position information for implicit type 2021-08-26 08:07:16 -07:00
inductionErrors.lean chore: fix tests 2021-08-07 13:22:58 -07:00
inductionErrors.lean.expected.out fix: leftovers in the local context when applying induction 2021-03-27 19:42:22 -07:00
inductionGen.lean feat: improve generalizing at induction 2021-03-27 14:28:03 -07:00
inductionGen.lean.expected.out fix: leftovers in the local context when applying induction 2021-03-27 19:42:22 -07:00
inductive1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
inductive1.lean.expected.out fix: pp.analyze mvars can bottom-up 2021-08-03 09:13:18 +02:00
infoFromFailure.lean
infoFromFailure.lean.expected.out feat: improved name-unresolving in delab 2021-09-07 16:26:00 +02:00
infoTree.lean fix: move elabCommand parts that should happen only once into new function 2021-06-29 06:34:15 -07:00
infoTree.lean.expected.out feat: convert "orphan" kernel nat literals n into ofNat n 2021-09-08 14:58:13 -07:00
inst.lean
inst.lean.expected.out
intModBug.lean
intModBug.lean.expected.out chore: fix test 2021-02-06 12:54:53 -08:00
intNegSucc.lean test: for Int.negSucc bug 2021-03-07 13:09:23 -08:00
intNegSucc.lean.expected.out test: for Int.negSucc bug 2021-03-07 13:09:23 -08:00
invalidFieldName.lean
invalidFieldName.lean.expected.out
invalidInstImplicit.lean feat: check instance implicit binder annotations 2021-04-28 17:15:08 -07:00
invalidInstImplicit.lean.expected.out feat: check instance implicit binder annotations 2021-04-28 17:15:08 -07:00
invalidNamedArgs.lean
invalidNamedArgs.lean.expected.out
IRbug.lean
IRbug.lean.expected.out
isDefEqOffsetBug.lean chore: fix tests 2021-05-04 15:42:03 -07:00
isDefEqOffsetBug.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
jason1.lean fix: missing error messages 2021-03-05 17:20:04 -08:00
jason1.lean.expected.out chore: fix tests 2021-08-03 09:13:18 +02:00
jason2.lean fix: missing error messages 2021-03-05 17:20:04 -08:00
jason2.lean.expected.out fix: missing error messages 2021-03-05 17:20:04 -08:00
json.lean
json.lean.expected.out fix: Json.num 2021-02-18 13:27:31 +01:00
kernelMVarBug.lean fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars 2021-08-04 16:58:00 -07:00
kernelMVarBug.lean.expected.out fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars 2021-08-04 16:58:00 -07:00
lazySeq.lean test: add *> laziness test 2021-09-07 18:03:15 -07:00
lazySeq.lean.expected.out test: add *> laziness test 2021-09-07 18:03:15 -07:00
letrec1.lean
letrec1.lean.expected.out
letrecErrors.lean
letrecErrors.lean.expected.out
liftOverLeft.lean fix: no method lift over let 2021-04-24 19:33:55 -07:00
liftOverLeft.lean.expected.out fix: no method lift over let 2021-04-24 19:33:55 -07:00
listLength.lean feat: use simple List.length definition and add csimp theorem 2021-08-21 13:11:06 -07:00
listLength.lean.expected.out feat: use simple List.length definition and add csimp theorem 2021-08-21 13:11:06 -07:00
ll_infer_type_bug.lean
ll_infer_type_bug.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
localNotationPP.lean fix: unexpanders should inherit scopedness 2021-03-13 13:20:12 +01:00
localNotationPP.lean.expected.out fix: unexpanders should inherit scopedness 2021-03-13 13:20:12 +01:00
loopErrorRecovery.lean fix: loop due to error recovery 2021-04-13 08:12:39 -07:00
loopErrorRecovery.lean.expected.out fix: loop due to error recovery 2021-04-13 08:12:39 -07:00
lvl1.lean
lvl1.lean.expected.out
macroPrio.lean
macroPrio.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
macroResolveName.lean feat: add Macro.resolveGlobalName and Macro.resolveNamespace? 2021-04-23 19:38:56 -07:00
macroResolveName.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
macroscopes.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
macroscopes.lean.expected.out
macroStack.lean
macroStack.lean.expected.out chore: fix tests 2021-08-13 17:24:58 -07:00
macroTrace.lean feat: trace support for MacroM 2021-04-23 19:15:14 -07:00
macroTrace.lean.expected.out feat: trace support for MacroM 2021-04-23 19:15:14 -07:00
mangling.lean fix: 32-bit Unicode name mangling 2021-06-23 00:08:20 -07:00
mangling.lean.expected.out fix: make mangling injective again 2021-06-23 00:08:20 -07:00
match1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
match1.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
match2.lean feat: match auto generalization 2021-04-16 21:48:38 -07:00
match2.lean.expected.out feat: match auto generalization 2021-04-16 21:48:38 -07:00
match3.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
match3.lean.expected.out
match4.lean chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
match4.lean.expected.out
matchAltIndent.lean fix: add checkColGe to matchAlt 2021-03-12 11:06:07 -08:00
matchAltIndent.lean.expected.out fix: add checkColGe to matchAlt 2021-03-12 11:06:07 -08:00
matchApp.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
matchApp.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
matchErrorLocation.lean
matchErrorLocation.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
matchErrorMsg.lean
matchErrorMsg.lean.expected.out
matchMissingCasesAsStuckError.lean fix: better error message when cases fails and there are no alternatives 2021-03-26 16:28:21 -07:00
matchMissingCasesAsStuckError.lean.expected.out fix: better error message when cases fails and there are no alternatives 2021-03-26 16:28:21 -07:00
matchOfNatIssue.lean feat: convert "orphan" kernel nat literals n into ofNat n 2021-09-08 14:58:13 -07:00
matchOfNatIssue.lean.expected.out feat: convert "orphan" kernel nat literals n into ofNat n 2021-09-08 14:58:13 -07:00
matchunit.lean chore: special support for match d with | PUnit.unit => rhs 2021-02-10 09:54:12 -08:00
matchunit.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
matchUnknownFVarBug.lean fix: ensure discriminants are distinct variables 2021-03-26 16:28:21 -07:00
matchUnknownFVarBug.lean.expected.out feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
missingExplicitWithForwardNamedDep.lean
missingExplicitWithForwardNamedDep.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
mkProjStx.lean feat: add mkProjStx? 2021-08-12 05:41:00 -07:00
mkProjStx.lean.expected.out feat: add mkProjStx? 2021-08-12 05:41:00 -07:00
modBug.lean chore: fix tests 2021-08-07 13:22:58 -07:00
modBug.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
moduleDoc.lean test: add test for getModuleDoc? 2021-08-06 14:14:22 -07:00
moduleDoc.lean.expected.out test: add test for getModuleDoc? 2021-08-06 14:14:22 -07:00
moduleOf.lean
moduleOf.lean.expected.out
mulcommErrorMessage.lean feat: improve error message and include variables introduced by the implicit lambda notation 2021-04-24 21:34:42 -07:00
mulcommErrorMessage.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
multiConstantError.lean feat: improve error message for constant a b c : Nat 2021-08-26 08:26:33 -07:00
multiConstantError.lean.expected.out feat: improve error message for constant a b c : Nat 2021-08-26 08:26:33 -07:00
mutualdef1.lean
mutualdef1.lean.expected.out
mutualWithNamespaceMacro.lean
mutualWithNamespaceMacro.lean.expected.out
mvar1.lean chore: fix tests 2021-09-07 19:14:30 -07:00
mvar1.lean.expected.out
mvar2.lean chore: fix tests 2021-09-07 19:14:30 -07:00
mvar2.lean.expected.out
mvar3.lean chore: fix tests 2021-09-07 19:14:30 -07:00
mvar3.lean.expected.out
mvar_fvar.lean chore: fix tests 2021-09-07 19:14:30 -07:00
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean fix: throw error when default value contains metavariables 2021-02-20 11:31:56 -08:00
mvarAtDefaultValue.lean.expected.out fix: throw error when default value contains metavariables 2021-02-20 11:31:56 -08:00
namedHoles.lean
namedHoles.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
namelit.lean feat: delab Name.mkStr/Num 2021-05-19 09:21:52 +02:00
namelit.lean.expected.out
negFloat.lean
negFloat.lean.expected.out
newCatPanic.lean fix: fixes #447 2021-05-08 19:04:12 -07:00
newCatPanic.lean.expected.out fix: fixes #447 2021-05-08 19:04:12 -07:00
nonAtomicFieldName.lean fix: ensure field names are atomic 2021-08-09 19:01:08 -07:00
nonAtomicFieldName.lean.expected.out fix: ensure field names are atomic 2021-08-09 19:01:08 -07:00
nondepArrow.lean fix: non-dependent arrow should not extend local context 2021-06-29 06:31:37 -07:00
nondepArrow.lean.expected.out fix: non-dependent arrow should not extend local context 2021-06-29 06:31:37 -07:00
nonReserved.lean
nonReserved.lean.expected.out
noTabs.lean test: forgot tabs ban test 2021-04-26 17:09:48 +02:00
noTabs.lean.expected.out test: forgot tabs ban test 2021-04-26 17:09:48 +02:00
notationPrecheck.lean feat: notation: unfold to prechecked quotation 2021-04-27 16:38:37 -07:00
notationPrecheck.lean.expected.out fix: avoid "failed to evaluate" error when extension has sorry 2021-05-04 20:57:53 -07:00
openExport.lean
openExport.lean.expected.out
openScoped.lean chore: elaborate open scoped 2021-08-21 07:16:24 -07:00
openScoped.lean.expected.out chore: elaborate open scoped 2021-08-21 07:16:24 -07:00
or_shortcircuit.lean chore: fix tests 2021-03-11 11:35:51 -08:00
or_shortcircuit.lean.expected.out
parserPrio.lean chore: two comments about bad pp.analyze behavior 2021-08-03 09:13:18 +02:00
parserPrio.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
partialVariable.lean fix: panic on variable : 2021-04-23 09:24:35 +02:00
partialVariable.lean.expected.out feat: add strict implicit binder annotation 2021-08-03 19:10:51 -07:00
patvar.lean
patvar.lean.expected.out fix: another antipattern 2021-04-07 10:42:54 -07:00
phashmap_inst_coherence.lean chore: fix test 2021-06-02 10:03:12 -07:00
phashmap_inst_coherence.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
ppExpr.lean fix: bug in ppExpr test 2021-08-03 09:13:18 +02:00
ppExpr.lean.expected.out fix: bug in ppExpr test 2021-08-03 09:13:18 +02:00
PPInstances.lean feat: pp.instances and pp.instanceTypes 2021-08-12 09:33:30 +02:00
PPInstances.lean.expected.out feat: pp.instances and pp.instanceTypes 2021-08-12 09:33:30 +02:00
ppite.lean
ppite.lean.expected.out fix: parenthesizer: respect lhsPrec 2021-08-03 15:22:08 +02:00
pplevel.lean chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
pplevel.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
ppMotives.lean feat: pp motives and misc delab fixes 2021-06-13 00:06:27 +02:00
ppMotives.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
ppNotationCode.lean fix: make precedence mandatory for mixfix commands 2021-07-19 13:18:58 -07:00
ppNotationCode.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
ppProofs.lean feat: pp.analyze isSubstLike support Eq.rec 2021-08-03 09:13:18 +02:00
ppProofs.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
PPRoundtrip.lean fix: formatter: check for comment tokens 2021-08-11 17:37:18 +02:00
PPRoundtrip.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
ppSyntax.lean
ppSyntax.lean.expected.out
precissues.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
precissues.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
private.lean
private.lean.expected.out
privateFieldCopyIssue.lean fix: propagate visibility annotation 2021-08-10 15:34:07 -07:00
privateFieldCopyIssue.lean.expected.out fix: propagate visibility annotation 2021-08-10 15:34:07 -07:00
Process.lean feat: IO.Process.Child.takeStdin 2021-06-11 17:53:51 -07:00
Process.lean.expected.out feat: IO.Process.Child.takeStdin 2021-06-11 17:53:51 -07:00
protected.lean
protected.lean.expected.out
pureCoeIssue.lean
pureCoeIssue.lean.expected.out fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
readDir.lean feat: make FilePath a concrete type 2021-05-28 14:19:59 +02:00
readDir.lean.expected.out feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
readlinkf.sh
redundantAlt.lean
redundantAlt.lean.expected.out
ref1.lean
ref1.lean.expected.out
Reformat.lean chore: fix tests 2021-08-06 14:05:00 -07:00
Reformat.lean.expected.out chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
renameBug.lean fix: nasty bug at rename tactic 2021-08-25 15:27:29 -07:00
renameBug.lean.expected.out fix: nasty bug at rename tactic 2021-08-25 15:27:29 -07:00
repr.lean
repr.lean.expected.out
repr_issue.lean
repr_issue.lean.expected.out
resolveGlobalName.lean
resolveGlobalName.lean.expected.out
revertlet.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
revertlet.lean.expected.out
rewrite.lean fix: rw: add all uninstantiated mvars as goals 2021-05-19 07:31:50 -07:00
rewrite.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
runSTBug.lean
runSTBug.lean.expected.out
safeShadowing.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
safeShadowing.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
sanitychecks.lean
sanitychecks.lean.expected.out
scopedInstanceOutsideNamespace.lean
scopedInstanceOutsideNamespace.lean.expected.out
scopedLocalInsts.lean
scopedLocalInsts.lean.expected.out
scopedMacros.lean feat: add scoped macro_rules (#432) 2021-04-30 09:05:09 +02:00
scopedMacros.lean.expected.out feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
scopedTokens.lean
scopedTokens.lean.expected.out
scopedunifhint.lean
scopedunifhint.lean.expected.out feat: pp.analyze original mvars are not unknown 2021-08-03 09:13:18 +02:00
shadow.lean
shadow.lean.expected.out fix: non-dependent arrow should not extend local context 2021-06-29 06:31:37 -07:00
simpArgTypeMismatch.lean chore: fix tests 2021-08-07 13:22:58 -07:00
simpArgTypeMismatch.lean.expected.out chore: fix tests 2021-08-07 13:22:58 -07:00
simpcfg.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
simpcfg.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
sizeof.lean
sizeof.lean.expected.out
smartUnfolding.lean
smartUnfolding.lean.expected.out
smartUnfoldingMatch.lean fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true 2021-08-17 21:32:32 -07:00
smartUnfoldingMatch.lean.expected.out fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true 2021-08-17 21:32:32 -07:00
sorryAtError.lean fix: bug at hasSyntheticSorry 2021-03-05 19:08:10 -08:00
sorryAtError.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
sorryWarning.lean
sorryWarning.lean.expected.out
stdio.lean
stdio.lean.expected.out
stream.lean chore: use polymorphic method forIn 2021-02-04 18:13:01 -08:00
stream.lean.expected.out
strictImplicit.lean feat: elaborate strict implicit binders 2021-08-03 19:40:44 -07:00
strictImplicit.lean.expected.out feat: elaborate strict implicit binders 2021-08-03 19:40:44 -07:00
string_imp.lean
string_imp.lean.expected.out
string_imp2.lean fix: Substring.splitOn 2021-07-19 09:55:37 +02:00
string_imp2.lean.expected.out fix: Substring.splitOn 2021-07-19 09:55:37 +02:00
struct1.lean feat: structure diamonds basic support 2021-08-09 19:01:08 -07:00
struct1.lean.expected.out chore: modify default value for option structureDiamondWarning 2021-08-10 09:24:53 -07:00
structAutoBound.lean
structAutoBound.lean.expected.out
structDefault.lean
structDefault.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
structDefValueOverride.lean feat: process overriden default values in copied parents 2021-08-10 18:55:12 -07:00
structDefValueOverride.lean.expected.out feat: process overriden default values in copied parents 2021-08-10 18:55:12 -07:00
structInst1.lean fix: check redundant sources at structure instance notation 2021-08-12 09:16:30 -07:00
structInst1.lean.expected.out fix: check redundant sources at structure instance notation 2021-08-12 09:16:30 -07:00
structInstError.lean
structInstError.lean.expected.out feat: pp.analyze detect when struct-inst type needed 2021-08-03 09:13:18 +02:00
structSorryBug.lean fix: error message 2021-03-11 12:16:15 -08:00
structSorryBug.lean.expected.out fix: error message 2021-03-11 12:16:15 -08:00
StxQuot.lean fix: syntax pattern match against multiple identifiers 2021-06-10 18:15:40 +02:00
StxQuot.lean.expected.out chore: disable pp.analyze for now 2021-09-07 07:51:43 -07:00
substlet.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
substlet.lean.expected.out fix: closes #421 2021-04-23 12:27:39 -07:00
syntaxErrors.lean
syntaxErrors.lean.expected.out
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.expected.out feat: delab Name.mkStr/Num 2021-05-19 09:21:52 +02:00
syntaxPrec.lean chore: align stx precedence in syntax to the new one in macro 2021-08-24 10:11:12 -07:00
syntaxPrec.lean.expected.out chore: fix test output 2021-09-05 17:49:03 -07:00
tacUnsolvedGoalsErrors.lean feat: move block tactic macro to Init 2021-05-21 17:13:33 -07:00
tacUnsolvedGoalsErrors.lean.expected.out feat: move block tactic macro to Init 2021-05-21 17:13:33 -07:00
tcloop.lean
tcloop.lean.expected.out chore: fix test output 2021-02-04 17:43:56 -08:00
test_single.sh
theoremType.lean
theoremType.lean.expected.out feat: improve error message 2021-03-05 13:42:54 -08:00
thunk.lean refactor: clean up Thunk 2021-04-22 20:29:08 -07:00
thunk.lean.expected.out refactor: clean up Thunk 2021-04-22 20:29:08 -07:00
toFieldNameIssue.lean fix: generation of to* field names 2021-08-11 17:25:02 -07:00
toFieldNameIssue.lean.expected.out fix: generation of to* field names 2021-08-11 17:25:02 -07:00
tokenErrors.lean chore: simplify tests 2021-04-05 22:01:56 +02:00
tokenErrors.lean.expected.out fix: make unterminated comments consume all input 2021-07-22 15:55:12 +02:00
tooManyVarsAtInduction.lean fix: report error if too many variable names have been provided at induction/cases alternative 2021-03-08 16:26:53 -08:00
tooManyVarsAtInduction.lean.expected.out feat: keep going if there are missing alternatives at induction/cases 2021-03-08 17:09:53 -08:00
typeIncorrectPat.lean
typeIncorrectPat.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
typeMismatch.lean
typeMismatch.lean.expected.out feat: include type of type in "mismatch errors" 2021-03-08 09:30:34 -08:00
typeOf.lean chore: fix tests 2021-03-11 11:35:51 -08:00
typeOf.lean.expected.out chore: fix tests 2021-08-13 17:24:58 -07:00
uintCtors.lean chore: fix tests 2021-08-07 13:22:58 -07:00
uintCtors.lean.expected.out
uintMatch.lean fix: pattern matching on UInt 2021-09-05 19:15:59 -07:00
uintMatch.lean.expected.out fix: pattern matching on UInt 2021-09-05 19:15:59 -07:00
unboxStruct.lean fix: unbox trivial unparameterized structures as well 2021-07-06 08:19:56 -07:00
unboxStruct.lean.expected.out chore: fix test 2021-07-06 17:28:09 +02:00
unexpandersNamespaces.lean chore: test unexpanders inside namespaces 2021-08-03 09:13:18 +02:00
unexpandersNamespaces.lean.expected.out chore: test unexpanders inside namespaces 2021-08-03 09:13:18 +02:00
UnexpandSubtype.lean feat: unexpander for Subtype 2021-08-12 09:32:33 +02:00
UnexpandSubtype.lean.expected.out feat: unexpander for Subtype 2021-08-12 09:32:33 +02:00
unhygienic.lean
unhygienic.lean.expected.out chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
unifHintAndTC.lean
unifHintAndTC.lean.expected.out feat: better bottom-up/structure-type heuristics 2021-08-03 09:13:18 +02:00
univInference.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
univInference.lean.expected.out
unknownId.lean
unknownId.lean.expected.out
unknownTactic.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
unknownTactic.lean.expected.out chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.expected.out
unsolvedIndCases.lean feat: improve generalizing at induction 2021-03-27 14:28:03 -07:00
unsolvedIndCases.lean.expected.out fix: leftovers in the local context when applying induction 2021-03-27 19:42:22 -07:00
unused_univ.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
unused_univ.lean.expected.out
whnfProj.lean chore: fix tests 2021-03-10 18:45:22 -08:00
whnfProj.lean.expected.out
zipper.lean
zipper.lean.expected.out