aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity
439 Commits 6 Branches 17 Tags 1.3 MiB
Commit Graph

439 Commits

Author SHA1 Message Date
Leni Aniva bd42c396d7
chore: Code cleanup 2024-05-20 14:19:10 -07:00
Leni Aniva bbc00cbbb8
feat: Congruence tactic FFI interface and tests 2024-05-20 14:00:04 -07:00
Leni Aniva 75df7268c5
test: Simplify testing structure for tactics 2024-05-20 11:55:38 -07:00
Leni Aniva 92acf7782c
test: CongruenceArg tactic 2024-05-20 11:51:35 -07:00
Leni Aniva cf1c884c8c
Merge branch 'dev' into goal/mapply 2024-05-20 11:08:14 -07:00
Leni Aniva cc74d41b15
feat: Congruence tactics 2024-05-20 10:55:52 -07:00
Leni Aniva 2f951c8fef
fix: Decoupling of mvars during instantiation 2024-05-19 15:43:10 -07:00
Leni Aniva 0aec757601 Merge pull request 'doc: README.md fix' (#73) from doc/readme into dev 
Reviewed-on: #73
 2024-05-17 20:33:18 -07:00
Leni Aniva e05c01109c
Merge branch 'dev' into doc/readme 2024-05-17 20:32:56 -07:00
Leni Aniva e165e41efa
chore: Version bump to v4.8.0-rc1 2024-05-17 20:31:45 -07:00
Leni Aniva 6ad24b72d4
fix: Nested delayed assignment instantiation 2024-05-16 10:31:38 -07:00
Leni Aniva cf17428001
fix: Panic in partial instantiation 2024-05-15 21:34:36 -07:00
Leni Aniva 5c7bb288b2
feat: Display full free variable list in subst 2024-05-14 19:09:04 -07:00
Leni Aniva bc09f4a29d
refactor: Expr related functions to Expr.lean 2024-05-13 13:58:50 -07:00
Leni Aniva f813d4a8dd
refactor: Delayed mvar instantiation function 2024-05-13 13:49:05 -07:00
Leni Aniva c04b363de7
feat: Handle delay assigned mvars 2024-05-12 22:33:38 -07:00
Leni Aniva 03ecb6cf19
feat: Partial instantiate metavariables 2024-05-11 20:01:34 -07:00
Leni Aniva 0b88f6708e
test: Delayed mvar assignment for mapply 2024-05-09 14:02:43 -07:00
Leni Aniva e58dbc66a9
fix: Consistent naming in library functions 2024-05-08 20:51:36 -07:00
Leni Aniva 66a5dfcf3c
feat: Diagnostics command for FFI users 2024-05-08 12:41:21 -07:00
Leni Aniva 69ec70ffbe
feat: Do not explicitly show delay assigned mvar 2024-05-06 22:39:17 -07:00
Leni Aniva aa106f7591
feat: Do not filter mvars from mapply 2024-05-06 22:20:20 -07:00
Leni Aniva 679871cbc6
fix: NoConfuse arg name 2024-05-05 13:26:46 -07:00
Leni Aniva 2937675044
feat: Library interface for calling no_confuse 2024-05-05 13:25:48 -07:00
Leni Aniva cf1289f159
feat: NoConfuse tactic 2024-05-05 13:24:29 -07:00
Leni Aniva 1e1995255a
test: mapply captures dependent types 2024-05-05 10:36:43 -07:00
Leni Aniva 63417ef179
fix: Motive extra arguments not instiantiated 2024-05-05 00:43:32 -07:00
Leni Aniva 4cff6677d2
chore: Lean version bump to 4.8.0-rc1 2024-05-04 23:36:42 -07:00
Leni Aniva 6ffb227cd6
feat: Conduit modus ponens 2024-04-22 10:02:09 -07:00
Leni Aniva feff62a3c5
fix: Remove determination of major 2024-04-22 09:52:13 -07:00
Leni Aniva 3812aa56ec
feat: Phantom var in mapply 2024-04-22 00:11:41 -07:00
Leni Aniva 4a92e655f6
test: Tactic test stub 2024-04-20 13:09:41 -07:00
Leni Aniva 398b1c39ed
refactor: Common tactic execute function 2024-04-19 12:37:17 -07:00
Leni Aniva fec13ddb51
chore: Code cleanup 2024-04-18 14:19:25 -07:00
Leni Aniva 7531ad628c
doc: Documentation about conditional arguments 2024-04-15 20:00:59 -07:00
Leni Aniva 52e5b5df50
doc: README.md fix 2024-04-15 19:57:05 -07:00
Leni Aniva 7aa7e6d7e9
feat: Library interface for mapply 2024-04-15 12:56:28 -07:00
Leni Aniva dbd54f7679
feat: Implement the mapply tactic 2024-04-15 12:47:02 -07:00
Leni Aniva 75b4648ba9
feat: mapply stub 2024-04-14 15:40:57 -07:00
Leni Aniva b954f12526
refactor: Move all tactic operations to the bottom 2024-04-13 19:41:49 -07:00
Leni Aniva adbb07af2d
fix: Option setting in REPL 2024-04-12 22:39:47 -07:00
Leni Aniva 72dd20ea87 Merge pull request 'feat: Let tactic' (#70) from goal/let into dev 
Reviewed-on: #70
 2024-04-12 21:42:32 -07:00
Leni Aniva 614b9aa4ae
Merge branch 'dev' into goal/let 2024-04-12 21:41:56 -07:00
Leni Aniva b45b90b810
test: Metavariable name matches in let 2024-04-12 21:41:16 -07:00
Leni Aniva 07094730b7 Merge pull request 'feat: Option to collect dependent metavariables' (#69) from serial/goal into dev 
Reviewed-on: #69
 2024-04-12 21:33:00 -07:00
Leni Aniva 77907fd060
feat: `goalLet` function 2024-04-12 21:30:56 -07:00
Leni Aniva 4ee955c21f
test: Tests the `let` tactic 2024-04-12 21:16:00 -07:00
Leni Aniva 4b01af7cef
Merge branch 'dev' into serial/goal 2024-04-12 20:52:38 -07:00
Leni Aniva 00a3613036 Merge pull request 'fix: Prevent incorrect inheritance of calc rhs' (#66) from goal/calc into dev 
Reviewed-on: #66
 2024-04-12 20:52:17 -07:00
Leni Aniva e5d55e31ff
feat: Print expression dependent mvars 2024-04-12 20:51:54 -07:00