lean4-htt/src/Lean/Util
2022-09-26 05:46:04 -07:00
..
CollectFVars.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
CollectLevelParams.lean feat: universe level parameter helper functions for the compiler 2022-09-17 16:29:44 -07:00
CollectMVars.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
FindExpr.lean chore: use new comment syntax 2022-09-14 08:26:17 -07:00
FindLevelMVar.lean chore: cleanup 2022-07-25 22:39:56 -07:00
FindMVar.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
FoldConsts.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
ForEachExpr.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
HasConstCache.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
MonadBacktrack.lean feat: add commitIfNoEx 2021-08-17 21:32:32 -07:00
MonadCache.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
OccursCheck.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
Path.lean refactor: use computed fields for Name 2022-07-11 14:19:41 -07:00
Paths.lean chore: unused variables 2022-07-07 20:24:18 -07:00
PPExt.lean chore: import reductions 2022-09-15 14:02:38 -07:00
Profile.lean chore: import reductions 2022-09-15 14:02:38 -07:00
RecDepth.lean
Recognizers.lean feat: add useRaw parameter at constructorApp? 2022-09-12 15:56:36 -07:00
ReplaceExpr.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
ReplaceLevel.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
SCC.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
ShareCommon.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Sorry.lean feat: trace nodes with messages 2022-08-15 08:55:25 -07:00
Trace.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00