Leonardo de Moura 1a5de2c184 feat: add reduceProjectionFn ... This is code for reducing user-facing projections functions created by the `structure` command.		2019-11-02 10:26:38 -07:00
..
Compiler
Elaborator
EqnCompiler
Parser
TypeClass	chore: use Level instead of Univ	2019-10-31 20:13:44 -07:00
AbstractMetavarContext.lean	chore: style	2019-10-31 11:34:34 -07:00
Attributes.lean
Class.lean
Declaration.lean	feat: helper functions	2019-10-31 20:58:30 -07:00
Default.lean
Environment.lean	feat: use CPS	2019-11-01 16:22:55 -07:00
Expr.lean	feat: helper functions	2019-11-01 17:07:26 -07:00
Format.lean
InductiveUtil.lean	feat: use CPS	2019-11-01 16:22:55 -07:00
KVMap.lean
LBool.lean	feat: add LBool	2019-10-30 19:30:08 -07:00
Level.lean
LocalContext.lean
Message.lean
MetavarContext.lean
Modifiers.lean
MonadCache.lean
Name.lean
NameGenerator.lean
Options.lean
Path.lean
Position.lean
ProjFns.lean	feat: add reduceProjectionFn	2019-11-02 10:26:38 -07:00
QuotUtil.lean	feat: use CPS	2019-11-01 16:22:55 -07:00
ReducibilityAttrs.lean
Runtime.lean
Scopes.lean
SMap.lean
Syntax.lean
TmpMetavarContext.lean
ToExpr.lean
Trace.lean
TypeUtil.lean	feat: reduce Expr.proj	2019-11-01 17:07:38 -07:00
Util.lean