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

• 52e5b5df50
  
  doc: README.md fix Leni Aniva 2024-04-15 19:57:05 -0700
• 7aa7e6d7e9
  
  feat: Library interface for mapply Leni Aniva 2024-04-15 12:56:28 -0700
• dbd54f7679
  
  feat: Implement the mapply tactic Leni Aniva 2024-04-15 12:47:02 -0700
• 75b4648ba9
  
  feat: mapply stub Leni Aniva 2024-04-14 15:40:57 -0700
• b954f12526
  
  refactor: Move all tactic operations to the bottom Leni Aniva 2024-04-13 19:41:49 -0700
• adbb07af2d
  
  fix: Option setting in REPL Leni Aniva 2024-04-12 22:39:47 -0700
• 72dd20ea87 Merge pull request 'feat: Let tactic' (#70) from goal/let into dev Leni Aniva 2024-04-12 21:42:32 -0700
• 614b9aa4ae
  
  Merge branch 'dev' into goal/let Leni Aniva 2024-04-12 21:41:56 -0700
• b45b90b810
  
  test: Metavariable name matches in let Leni Aniva 2024-04-12 21:41:16 -0700
• 07094730b7 Merge pull request 'feat: Option to collect dependent metavariables' (#69) from serial/goal into dev Leni Aniva 2024-04-12 21:33:00 -0700
• 77907fd060
  
  feat: `goalLet` function Leni Aniva 2024-04-12 21:30:56 -0700
• 4ee955c21f
  
  test: Tests the `let` tactic Leni Aniva 2024-04-12 21:16:00 -0700
• 4b01af7cef
  
  Merge branch 'dev' into serial/goal Leni Aniva 2024-04-12 20:52:38 -0700
• 00a3613036 Merge pull request 'fix: Prevent incorrect inheritance of calc rhs' (#66) from goal/calc into dev Leni Aniva 2024-04-12 20:52:17 -0700
• e5d55e31ff
  
  feat: Print expression dependent mvars Leni Aniva 2024-04-12 20:51:54 -0700
• 8e377c2092
  
  refactor: CamelCase rename Leni Aniva 2024-04-12 16:34:21 -0700
• 991ee5ad94
  
  refactor: Rename functions to camel case Leni Aniva 2024-04-12 12:37:37 -0700
• 7a4d462a87
  
  Merge branch 'dev' into goal/calc Leni Aniva 2024-04-11 17:58:45 -0700
• 4d4f660f3f
  
  chore: Update version Leni Aniva 2024-04-11 17:57:24 -0700
• a864c4d3ff
  
  refactor: Code simplification Leni Aniva 2024-04-11 16:29:47 -0700
• e834765896
  
  refactor: Code simplification Leni Aniva 2024-04-11 16:25:17 -0700
• dc6e79def7
  
  doc: Update error message in interaction Leni Aniva 2024-04-11 16:18:04 -0700
• 036fab0ad6
  
  fix: Prevent incorrect inheritance of calc rhs Leni Aniva 2024-04-11 16:11:06 -0700
• f20ee8dc87 Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59) from goal/have-conv-calc into dev Leni Aniva 2024-04-11 15:36:19 -0700
• 440cc1c920
  
  Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-11 15:35:30 -0700
• a41b95e540 Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-11 15:35:30 -0700
• e43601de4b feat: Print recursor rules Leni Aniva 2024-04-09 21:24:08 -0700
• a11df9f2e9 feat: Print recursor rules Leni Aniva 2024-04-09 21:24:08 -0700
• db35ec7187
  
  doc: New tactics in README.md Leni Aniva 2024-04-11 15:13:12 -0700
• ed220bc7fb doc: New tactics in README.md Leni Aniva 2024-04-11 15:13:12 -0700
• 327b402cdf
  
  feat: REPL interface for `calc` Leni Aniva 2024-04-11 15:11:10 -0700
• 7eb5419f36 feat: REPL interface for `calc` Leni Aniva 2024-04-11 15:11:10 -0700
• 222cb035d1
  
  feat: Add library bindings for calc Leni Aniva 2024-04-11 15:04:36 -0700
• 6d85c19589 feat: Add library bindings for calc Leni Aniva 2024-04-11 15:04:36 -0700
• 663651b10e
  
  fix: Remove `calcPrevRhs?` in non-calc tactics Leni Aniva 2024-04-11 15:03:14 -0700
• 6b44d9ef14 fix: Remove `calcPrevRhs?` in non-calc tactics Leni Aniva 2024-04-11 15:03:14 -0700
• 403d92692e
  
  feat: Calc tactic Leni Aniva 2024-04-11 14:59:55 -0700
• 535770bbd7 feat: Calc tactic Leni Aniva 2024-04-11 14:59:55 -0700
• a1599e6016
  
  Merge branch 'dev' into env/inspect Leni Aniva 2024-04-09 21:29:19 -0700
• 8198fe5424
  
  feat: Print recursor rules Leni Aniva 2024-04-09 21:24:08 -0700
• 823c9635c7 fix: Leading element in .proj sexp Leni Aniva 2024-04-09 10:06:26 -0700
• 56cfe523df
  
  fix: Leading element in .proj sexp Leni Aniva 2024-04-09 10:06:26 -0700
• 55b44c3fa1 fix: Serialization of .proj Leni Aniva 2024-04-09 10:03:36 -0700
• 9cc770c3c9
  
  fix: Serialization of .proj Leni Aniva 2024-04-09 10:03:36 -0700
• 100cdd885f
  
  fix: Coupling from unrelated goals Leni Aniva 2024-04-09 09:11:15 -0700
• 30c1fd894f fix: Coupling from unrelated goals Leni Aniva 2024-04-09 09:11:15 -0700
• 9a04fd4819
  
  feat: Focus command Leni Aniva 2024-04-08 13:12:51 -0700
• f02f9592d7 feat: Focus command Leni Aniva 2024-04-08 13:12:51 -0700
• dd94e29293
  
  refactor: Monads in library Leni Aniva 2024-04-08 12:54:02 -0700
• 0e63583a1d refactor: Monads in library Leni Aniva 2024-04-08 12:54:02 -0700
• 9fbc65829d
  
  feat: FFI interface to conv functions Leni Aniva 2024-04-08 12:50:41 -0700
• d4e49310f0 feat: FFI interface to conv functions Leni Aniva 2024-04-08 12:50:41 -0700
• f3a3ca31a0
  
  doc: Remove outdated comments Leni Aniva 2024-04-08 12:45:03 -0700
• 2f48cfbc19 doc: Remove outdated comments Leni Aniva 2024-04-08 12:45:03 -0700
• 73bdcb6be6
  
  refactor: Use the `tactic interface for `conv Leni Aniva 2024-04-08 12:32:27 -0700
• 22bb818a1c refactor: Use the `tactic interface for `conv Leni Aniva 2024-04-08 12:32:27 -0700
• 3094d11e48
  
  feat: Conv tactic functions Leni Aniva 2024-04-08 12:26:22 -0700
• 63e64a1e9f feat: Conv tactic functions Leni Aniva 2024-04-08 12:26:22 -0700
• ea0f411949
  
  Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-08 10:38:18 -0700
• 7af24a4f0a Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-08 10:38:18 -0700
• c629163aa1
  
  perf: Lazy run print monads Leni Aniva 2024-04-08 10:32:13 -0700
• 09189ce600 perf: Lazy run print monads Leni Aniva 2024-04-08 10:32:13 -0700
• ab0d87450a
  
  feat: Conv tactic mode Leni Aniva 2024-04-07 17:03:49 -0700
• 19d2f5ff3f feat: Conv tactic mode Leni Aniva 2024-04-07 17:03:49 -0700
• aba1d9be10
  
  refactor: Metavariable set diff function Leni Aniva 2024-04-07 14:32:25 -0700
• d50720f622 refactor: Metavariable set diff function Leni Aniva 2024-04-07 14:32:25 -0700
• 9d7c9598f5
  
  feat: Partial implementation of `conv` Leni Aniva 2024-04-07 14:22:20 -0700
• d9ed051b4d feat: Partial implementation of `conv` Leni Aniva 2024-04-07 14:22:20 -0700
• 5925b6163a
  
  Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-06 22:04:52 -0700
• 38cb91652f Merge branch 'dev' into goal/have-conv-calc Leni Aniva 2024-04-06 22:04:52 -0700
• be44eadde5 Merge pull request 'fix: Auto bound implicit in elab' (#60) from elab/level into dev Leni Aniva 2024-04-06 22:04:31 -0700
• 013cb8bb57 Merge pull request 'fix: Auto bound implicit in elab' (#60) from elab/level into dev Leni Aniva 2024-04-06 22:04:31 -0700
• aa8da3014e
  
  feat: The `have` tactic Leni Aniva 2024-04-06 21:52:25 -0700
• 7fe73551c3 feat: The `have` tactic Leni Aniva 2024-04-06 21:52:25 -0700
• d72a60f4e4
  
  fix: Auto bound implicit in elab Leni Aniva 2024-04-06 17:45:36 -0700
• 5a60ca74d5 fix: Auto bound implicit in elab Leni Aniva 2024-04-06 17:45:36 -0700
• 3db1207aa6
  
  test: Tests for conv and calc Leni Aniva 2024-04-06 17:22:09 -0700
• 41cb3f68cd test: Tests for conv and calc Leni Aniva 2024-04-06 17:22:09 -0700
• 951c2cec19
  
  feat: Bindings for the `have` tactic Leni Aniva 2024-04-06 16:40:22 -0700
• 058f5a98b2 feat: Bindings for the `have` tactic Leni Aniva 2024-04-06 16:40:22 -0700
• ace2ddf478
  
  feat: `GoalState.tryHave` tactic (tests failing) Leni Aniva 2024-04-06 16:33:20 -0700
• 1b7b6a644b feat: `GoalState.tryHave` tactic (tests failing) Leni Aniva 2024-04-06 16:33:20 -0700
• d44693e548
  
  doc: Documentation for `nix flake check` Leni Aniva 2024-04-06 14:15:58 -0700
• 042dc8f530 doc: Documentation for `nix flake check` Leni Aniva 2024-04-06 14:15:58 -0700
• fd47711e1f
  
  test: Move parallelism to Test/Main.lean Leni Aniva 2024-04-06 14:14:30 -0700
• 92351c9a3d test: Move parallelism to Test/Main.lean Leni Aniva 2024-04-06 14:14:30 -0700
• 4cbfc45292
  
  test: Parallel testing infrastructure Leni Aniva 2024-04-06 14:07:13 -0700
• 8a447e67cd test: Parallel testing infrastructure Leni Aniva 2024-04-06 14:07:13 -0700
• b1da7f2151 Merge pull request 'feat: Instantiate mvars during echo' (#56) from expr/echo into dev Leni Aniva 2024-03-31 17:10:29 -0700
• ed196494c1 Merge pull request 'feat: Instantiate mvars during echo' (#56) from expr/echo into dev Leni Aniva 2024-03-31 17:10:29 -0700
• 6f85c262cf
  
  feat: Instantiate mvars during echo Leni Aniva 2024-03-31 17:09:24 -0700
• 8b43dc0f25 feat: Instantiate mvars during echo Leni Aniva 2024-03-31 17:09:24 -0700
• 2511573a82 Merge pull request 'feat: Specify type in echo' (#55) from expr/echo into dev Leni Aniva 2024-03-31 16:45:43 -0700
• 744c9ee286 Merge pull request 'feat: Specify type in echo' (#55) from expr/echo into dev Leni Aniva 2024-03-31 16:45:43 -0700
• 2d422dc532 Merge pull request 'fix: Instantiation causes infinite loop' (#54) from output/expr into dev Leni Aniva 2024-03-31 16:43:53 -0700
• 9c8cc33e07 Merge pull request 'fix: Instantiation causes infinite loop' (#54) from output/expr into dev Leni Aniva 2024-03-31 16:43:53 -0700
• 2130bcf357
  
  test: Library test Leni Aniva 2024-03-31 16:43:30 -0700
• 216bb9e920 test: Library test Leni Aniva 2024-03-31 16:43:30 -0700
• 840d2acbd8
  
  docs: Update README.md Leni Aniva 2024-03-31 16:12:23 -0700
• f462843218 docs: Update README.md Leni Aniva 2024-03-31 16:12:23 -0700