Commit Graph

Select branches

Hide Pull Requests

dev

doc/rationale

goal/tactic

main

parse/level

serial/pickle

#10

#100

#101

#105

#107

#108

#109

#11

#110

#111

#113

#115

#116

#119

#12

#120

#121

#123

#13

#14

#15

#16

#17

#2

#20

#21

#25

#26

#27

#28

#29

#30

#31

#32

#33

#35

#36

#37

#38

#40

#41

#42

#43

#44

#45

#46

#47

#48

#49

#5

#50

#51

#52

#53

#54

#55

#56

#58

#59

#60

#63

#64

#65

#66

#68

#69

#7

#70

#71

#72

#73

#75

#76

#79

#81

#82

#83

#85

#86

#87

#89

#90

#91

#92

#94

#96

#99

0.1

0.2.3

v0.2.10

v0.2.10-alpha

v0.2.11

v0.2.12

v0.2.13

v0.2.14

v0.2.18

v0.2.19

v0.2.19-alpha

v0.2.20

v0.2.5

v0.2.6

v0.2.7

v0.2.8

v0.2.9

Mono Color

• d17b21e282
  
  fix: Use `getMVarsNoDelayed` Leni Aniva 2024-08-16 00:32:34 -0700
• 5b4f8a37eb
  
  refactor: All Tactic/ tactics into MetaM form Leni Aniva 2024-08-15 23:41:17 -0700
• 1e7a186bb1
  
  refactor: MetaM form of define (evaluate) Leni Aniva 2024-08-15 23:23:17 -0700
• 9b0456a5e0
  
  refactor: MetaM form of have and let Leni Aniva 2024-08-15 23:17:15 -0700
• 7968072097
  
  refactor: Remove the newMVarSet mechanism Leni Aniva 2024-08-15 22:53:42 -0700
• e07f9d9b3f
  
  Merge branch 'dev' into tactic/eval Leni Aniva 2024-08-15 22:45:43 -0700
• 56100a30af Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev Leni Aniva 2024-08-15 22:41:58 -0700
• e943a4b065
  
  refactor: Assign into its own tactic Leni Aniva 2024-08-15 22:39:40 -0700
• 0bc7bc5856
  
  refactor: Remove export of Lean functions Leni Aniva 2024-08-14 01:20:56 -0700
• caac70f0cf
  
  feat: Move non package outputs to dependencies Leni Aniva 2024-08-04 17:52:36 -0700
• 64269868d5
  
  feat: Expose project and leanPkgs in flake Leni Aniva 2024-08-04 17:32:20 -0700
• c9ee31bbfd
  
  feat: Export `mkFun` Leni Aniva 2024-08-02 22:33:03 -0700
• 394fb73137
  
  feat: Add direct expression to string Leni Aniva 2024-08-02 22:00:27 -0700
• c0e2a592ea
  
  feat: Expose `mkAppM'` Leni Aniva 2024-08-02 21:44:46 -0700
• 2c08ef1e23
  
  refactor: Remove old `visibleFVars` interface Leni Aniva 2024-08-02 19:53:19 -0700
• 651afa75f4
  
  feat: Filter in `visibleFVarsOfMVar` Leni Aniva 2024-08-02 19:49:11 -0700
• abef7a6f0d
  
  feat: Export fvar names function Leni Aniva 2024-07-31 00:00:21 -0700
• caa463f410
  
  feat: Export GoalState.goalsArray Leni Aniva 2024-07-30 17:02:41 -0700
• 3ca52517ab
  
  feat: Refactor out projToApp Leni Aniva 2024-07-30 13:30:41 -0700
• 1c9a411d4d
  
  feat: Export constant info type/value Leni Aniva 2024-07-29 18:39:22 -0700
• 7b5567d784
  
  fix: Name internal order Leni Aniva 2024-07-28 14:19:47 -0700
• 29f437f859
  
  feat: Export GoalState.create Leni Aniva 2024-07-28 13:58:20 -0700
• 4c81f226d1
  
  feat: Expose environment functions Leni Aniva 2024-07-28 13:46:14 -0700
• 9db5463499
  
  feat: Export `GoalState.resume` Leni Aniva 2024-07-27 18:20:34 -0700
• bf941cd686
  
  feat: Expose parent and root expr functions Leni Aniva 2024-07-27 17:39:51 -0700
• 2682ce5b7b
  
  refactor: Move condensed functions to condensed Leni Aniva 2024-07-23 11:57:12 -0700
• 3b415e8dc1
  
  chore: Rename exports Leni Aniva 2024-07-23 05:16:46 -0700
• 431ca4e481
  
  fix: Move elab context to condensed Leni Aniva 2024-07-22 17:57:01 -0700
• eb5ee8c57c
  
  feat: Expose TermElab context and state Leni Aniva 2024-07-22 17:34:14 -0700
• 94c7b021f7
  
  fix: Signature of ppExpr Leni Aniva 2024-07-15 12:22:47 -0700
• 193d94e798
  
  feat: Expression creation and pretty printing Leni Aniva 2024-07-15 11:42:02 -0700
• a7fe7cbd7c
  
  Merge branch 'misc/version' into serial/expr Leni Aniva 2024-07-15 09:53:36 -0700
• df8b6602ee
  
  Merge branch 'misc/version' into tactic/eval Leni Aniva 2024-07-06 20:00:12 -0700
• 9b1dd0ffda
  
  chore: Update flake Leni Aniva 2024-07-06 19:58:55 -0700
• 4549ae1f65
  
  Merge branch 'misc/version' into tactic/eval Leni Aniva 2024-07-06 19:56:31 -0700
• c404564a2b
  
  chore: Bump Lean version to 4.10.0-rc1 Leni Aniva 2024-07-06 19:53:50 -0700
• 6ddde2963d
  
  test: Eval instantiate Leni Aniva 2024-06-27 14:51:16 -0400
• fc0d872343
  
  refactor: Simplify proof test infrastructure Leni Aniva 2024-06-27 14:34:21 -0400
• 2d2ff24017
  
  feat: FFI interface for `evaluate` tactic Leni Aniva 2024-06-25 17:01:49 -0400
• 7acf1ffdf1
  
  refactor: Move `have` to prograde tactic Leni Aniva 2024-06-25 16:58:35 -0400
• 58f9d72288
  
  test: Evaluate tactic context Leni Aniva 2024-06-25 16:18:31 -0400
• c0124b347f
  
  Merge branch 'serial/expr' into tactic/eval Leni Aniva 2024-06-25 16:05:20 -0400
• 8e78718447
  
  feat: Extract MetaM context and state from goal Leni Aniva 2024-06-25 15:54:55 -0400
• ffbea41f62
  
  feat: Condensed interface Leni Aniva 2024-06-25 15:13:58 -0400
• e282d9f781
  
  test: Evaluation tactic Leni Aniva 2024-06-25 11:03:08 -0400
• 25a7025c25
  
  feat: Evaluation tactic Leni Aniva 2024-06-23 15:01:51 -0700
• 472cd54868 Merge pull request 'refactor: Cleanup the congruence tactics' (#81) from tactic/congruence into dev Leni Aniva 2024-06-23 13:35:36 -0700
• fbe6e8fcb3
  
  Merge branch 'dev' into tactic/congruence Leni Aniva 2024-06-23 13:35:07 -0700
• 361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev Leni Aniva 2024-06-23 13:33:35 -0700
• aceee85b05
  
  Merge branch 'env/inspect' into tactic/congruence Leni Aniva 2024-06-16 13:46:18 -0700
• 8707dbc9bb
  
  fix: aux lemmas in env inspect Leni Aniva 2024-06-16 13:44:57 -0700
• f80d90ce87
  
  fix: Goal diag missing newline character Leni Aniva 2024-06-14 11:58:23 -0700
• b3a60fcea8
  
  refactor: Rename TacticExecute to SyntheticTactic Leni Aniva 2024-06-13 14:24:22 -0700
• bd20bf76da Merge pull request 'feat: Elementarized tactics with motives, congruence, and absurdity' (#72) from goal/mapply into dev Leni Aniva 2024-06-12 13:52:45 -0700
• 2d2cf75183
  
  Merge branch 'dev' into goal/mapply Leni Aniva 2024-06-12 13:44:49 -0700
• c0e6e3ec39
  
  Merge branch 'parse/level' into goal/mapply Leni Aniva 2024-06-11 15:21:35 -0700
• 773a0afbd8
  
  feat: Handling of universe level names in elab parse/level Leni Aniva 2024-06-11 12:44:42 -0700
• 3a53493089
  
  feat: Show delayed assignment in goal diag Leni Aniva 2024-06-05 16:14:52 -0700
• 6dcff8b151
  
  fix: Print diag in mvar context Leni Aniva 2024-06-05 15:56:20 -0700
• 3c90c94645
  
  fix: Execute instantiateAll in goal state diag Leni Aniva 2024-06-05 13:45:13 -0700
• 67e7f22b0a Merge pull request 'feat: Extraction of tactics from compiler' (#76) from compile/tactic into dev Leni Aniva 2024-05-31 20:23:50 -0700
• a2c5c7448c
  
  chore: Code simplification, version bump Leni Aniva 2024-05-31 20:22:16 -0700
• 855e771609
  
  feat: Add compilation unit boundary command Leni Aniva 2024-05-31 16:35:46 -0700
• b9b16ba0e9
  
  refactor: Code cleanup Leni Aniva 2024-05-28 20:24:23 -0700
• 09628309a9
  
  feat: Basic tactic extraction (before/after/tactic) Leni Aniva 2024-05-28 17:25:22 -0700
• bd42c396d7
  
  chore: Code cleanup Leni Aniva 2024-05-20 14:19:10 -0700
• bbc00cbbb8
  
  feat: Congruence tactic FFI interface and tests Leni Aniva 2024-05-20 14:00:04 -0700
• 75df7268c5
  
  test: Simplify testing structure for tactics Leni Aniva 2024-05-20 11:55:38 -0700
• 92acf7782c
  
  test: CongruenceArg tactic Leni Aniva 2024-05-20 11:51:35 -0700
• cf1c884c8c
  
  Merge branch 'dev' into goal/mapply Leni Aniva 2024-05-20 11:08:14 -0700
• cc74d41b15
  
  feat: Congruence tactics Leni Aniva 2024-05-20 10:55:52 -0700
• 2f951c8fef
  
  fix: Decoupling of mvars during instantiation Leni Aniva 2024-05-19 15:43:10 -0700
• 0aec757601 Merge pull request 'doc: README.md fix' (#73) from doc/readme into dev Leni Aniva 2024-05-17 20:33:18 -0700
• e05c01109c
  
  Merge branch 'dev' into doc/readme Leni Aniva 2024-05-17 20:32:56 -0700
• e165e41efa
  
  chore: Version bump to v4.8.0-rc1 Leni Aniva 2024-05-17 20:31:45 -0700
• 6ad24b72d4
  
  fix: Nested delayed assignment instantiation Leni Aniva 2024-05-16 10:31:38 -0700
• cf17428001
  
  fix: Panic in partial instantiation Leni Aniva 2024-05-15 21:34:15 -0700
• 5c7bb288b2
  
  feat: Display full free variable list in subst Leni Aniva 2024-05-14 19:08:25 -0700
• bc09f4a29d
  
  refactor: Expr related functions to Expr.lean Leni Aniva 2024-05-13 13:58:50 -0700
• f813d4a8dd
  
  refactor: Delayed mvar instantiation function Leni Aniva 2024-05-13 13:49:05 -0700
• c04b363de7
  
  feat: Handle delay assigned mvars Leni Aniva 2024-05-12 22:33:38 -0700
• 03ecb6cf19
  
  feat: Partial instantiate metavariables Leni Aniva 2024-05-11 20:01:02 -0700
• 0b88f6708e
  
  test: Delayed mvar assignment for mapply Leni Aniva 2024-05-09 14:02:43 -0700
• e58dbc66a9
  
  fix: Consistent naming in library functions Leni Aniva 2024-05-08 20:51:36 -0700
• 66a5dfcf3c
  
  feat: Diagnostics command for FFI users Leni Aniva 2024-05-08 12:41:21 -0700
• 69ec70ffbe
  
  feat: Do not explicitly show delay assigned mvar Leni Aniva 2024-05-06 22:39:17 -0700
• aa106f7591
  
  feat: Do not filter mvars from mapply Leni Aniva 2024-05-06 22:20:20 -0700
• 679871cbc6
  
  fix: NoConfuse arg name Leni Aniva 2024-05-05 13:26:46 -0700
• 2937675044
  
  feat: Library interface for calling no_confuse Leni Aniva 2024-05-05 13:25:48 -0700
• cf1289f159
  
  feat: NoConfuse tactic Leni Aniva 2024-05-05 13:24:29 -0700
• 1e1995255a
  
  test: mapply captures dependent types Leni Aniva 2024-05-05 10:36:43 -0700
• 63417ef179
  
  fix: Motive extra arguments not instiantiated Leni Aniva 2024-05-05 00:43:32 -0700
• 4cff6677d2
  
  chore: Lean version bump to 4.8.0-rc1 Leni Aniva 2024-05-04 23:36:42 -0700
• 6ffb227cd6
  
  feat: Conduit modus ponens Leni Aniva 2024-04-22 10:02:09 -0700
• feff62a3c5
  
  fix: Remove determination of major Leni Aniva 2024-04-22 09:52:13 -0700
• 3812aa56ec
  
  feat: Phantom var in mapply Leni Aniva 2024-04-22 00:11:41 -0700
• 4a92e655f6
  
  test: Tactic test stub Leni Aniva 2024-04-20 13:09:41 -0700
• 398b1c39ed
  
  refactor: Common tactic execute function Leni Aniva 2024-04-19 12:37:17 -0700
• fec13ddb51
  
  chore: Code cleanup Leni Aniva 2024-04-18 14:19:25 -0700
• 7531ad628c
  
  doc: Documentation about conditional arguments Leni Aniva 2024-04-15 20:00:59 -0700