max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Leonardo de Moura 5854b5b9fe feat: disallow alternatives of the form | _ ids => ... 
@Kha We are still accepting wildcard alternatives of the form
     `| _ => ...`
It is useful when we can discharge many alternatives using the same
tactic, and it looks like the wildcard alternative used in "match"-expressions.
2020-11-02 19:23:30 -08:00
..
Compiler chore: use new termFor, termReturn, termTry, and tryUnless 2020-10-31 19:19:18 -07:00
Data chore: naming convention 2020-10-31 19:19:18 -07:00
Elab feat: disallow alternatives of the form | _ ids => ... 2020-11-02 19:23:30 -08:00
Meta feat: improve getElimInfo 2020-11-02 18:45:52 -08:00
Parser feat: extend cases tactic syntax 2020-11-02 16:46:33 -08:00
ParserCompiler chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
PrettyPrinter feat: better error message for "unknown" tactic 2020-10-30 14:58:17 -07:00
Server chore: remove old frontend leftovers 2020-10-26 09:08:07 -07:00
Util chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
Attributes.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
AuxRecursor.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Class.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Compiler.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
CoreM.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Declaration.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Delaborator.lean chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
Elab.lean chore: remove StrategyAttrs 2020-11-02 06:39:21 -08:00
Environment.lean chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
Eval.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Exception.lean chore: cleanup 2020-10-29 10:24:16 -07:00
Expr.lean chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
HeadIndex.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Hygiene.lean chore: cleanup 2020-10-28 09:33:19 -07:00
InternalExceptionId.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
KeyedDeclsAttribute.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Level.lean chore: cleanup 2020-10-29 10:24:16 -07:00
LocalContext.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Message.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
Meta.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
MetavarContext.lean chore: remove Expr.localE constructor 2020-11-01 09:37:48 -08:00
Modifiers.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
MonadEnv.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Parser.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
ParserCompiler.lean chore: remove clutter 2020-10-28 14:11:06 -07:00
PrettyPrinter.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
ProjFns.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
ReducibilityAttrs.lean refactor: add polymorphic methods for updating/querying reducibility status 2020-10-26 17:07:28 -07:00
ResolveName.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Runtime.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Server.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
Structure.lean chore: cleanup 2020-10-28 09:33:19 -07:00
Syntax.lean chore: use Subarray combinators 2020-10-28 19:52:59 -07:00
ToExpr.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Util.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00