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

192 Commits

Author SHA1 Message Date
Leni Aniva 8b67e7006a
feat: Add lake and lean to the package output 2024-02-05 11:50:22 -08:00
Leni Aniva 4a98b90289
chore: Version bump to 0.2.12-alpha 2024-01-30 17:45:32 -08:00
Leni Aniva 5720c72515
feat: Prevent crash during rootExpr call 2024-01-30 17:22:20 -08:00
Leni Aniva 6d22841a27
doc: Correct comment about parent filling expr 2024-01-30 16:37:35 -08:00
Leni Aniva 9a5ee49778
feat: Print parent expression assignment 2024-01-24 18:19:04 -08:00
Leni Aniva a811decf84 Merge pull request 'test: Option controlled mvar instantiation' (#44) from goal/diag into dev 
Reviewed-on: #44
 2024-01-17 22:27:44 -08:00
Leni Aniva 79b6974172
Merge branch 'dev' into goal/diag 2024-01-17 14:03:19 -08:00
Leni Aniva 42c3da4a67 Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43) from env/inspect into dev 
Reviewed-on: #43
 2024-01-17 14:02:55 -08:00
Leni Aniva efa956464d
test: Option controlled mvar instantiation 2024-01-16 16:44:54 -08:00
Leni Aniva 93a34f9fda
feat: Print constructor and recursor info 2024-01-16 14:11:52 -08:00
Leni Aniva a1421439f8
feat: Print inductives in env.inspect 2024-01-16 13:29:30 -08:00
Leni Aniva b29f7cb180
test: Simplify monad execution 2024-01-07 14:14:20 -08:00
Leni Aniva 6e39b5ef8b Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev 
Reviewed-on: #41
 2023-12-26 12:41:01 -08:00
Leni Aniva 77232d5a1e
refactor: Rename Test/{Catalog,Environment} 2023-12-26 12:22:57 -05:00
Leni Aniva 22789436bd
chore: Move environment functions to its own file 
Symbol.lean is now subsumed
 2023-12-15 13:40:36 -05:00
Leni Aniva aca7dc9811
refactor: env. operations into its own file 2023-12-15 13:37:55 -05:00
Leni Aniva 3b83c81540
fix: Force instantiate all mvars in env.add 2023-12-15 13:07:59 -05:00
Leni Aniva 6c25cca46a
test: env.add 2023-12-14 11:11:24 -08:00
Leni Aniva 2f3a91562a
fix: env_add monads 2023-12-14 05:52:12 -08:00
Leni Aniva 09f5792d4a
Merge branch 'dev' into env/add-decl 2023-12-14 05:48:49 -08:00
Leni Aniva 4076d8a7dd Merge pull request 'feat: Change the main interaction monad' (#40) from core/loop into dev 
Reviewed-on: #40
 2023-12-14 05:46:39 -08:00
Leni Aniva 02889510b2
feat: env_add command 2023-12-13 19:35:32 -08:00
Leni Aniva 12544b81ee
chore: Rename lib. commands to env. 
This is done to improve clarity and align with Lean's terminology
 2023-12-12 18:56:25 -08:00
Leni Aniva ab1b309c72
feat: Use CoreM as the main interaction monad 2023-12-12 18:39:02 -08:00
Leni Aniva 45beca0bc4
doc: TermElabM metavariable generation 2023-12-08 17:32:30 -08:00
Leni Aniva 1fb189a38f
fix: Consolidate TermElabM blocks 2023-12-08 17:31:25 -08:00
Leni Aniva c76751861a
fix: Change the main interaction monad to MetaM 2023-12-08 16:17:16 -08:00
Leni Aniva de2688ccfa
chore: Version downgrade to 0.2.10-alpha 
There is a currently known bug
 2023-12-07 12:38:02 -08:00
Leni Aniva 4871133027 Merge pull request 'fix: Printing projection leads to crash' (#37) from io/sexp into dev 
Reviewed-on: #37
 2023-12-07 12:33:01 -08:00
Leni Aniva 2dc7657e2a
doc: getUsedConstants bug about projections 2023-12-06 15:05:04 -08:00
Leni Aniva ccf5a03647
fix: Printing projection leads to crash 2023-12-05 22:45:59 -08:00
Leni Aniva 56966b27cf Merge pull request 'feat: Handling of private names' (#36) from library/catalog into dev 
Reviewed-on: #36
 2023-12-05 20:22:38 -08:00
Leni Aniva 9276d47e0d
Merge branch 'dev' into library/catalog 2023-12-05 20:21:22 -08:00
Leni Aniva cf856d2880
chore: Version bump 2023-12-05 20:21:07 -08:00
Leni Aniva beb837ccab Merge pull request 'feat: Print structural projection as application' (#35) from io/serial into dev 
Reviewed-on: #35
 2023-12-05 20:20:51 -08:00
Leni Aniva da74258dd1
feat!: Display public name only if name is private 2023-12-05 20:20:08 -08:00
Leni Aniva 9f2b07757f
feat: Display whether a symbol is private 2023-12-05 19:07:00 -08:00
Leni Aniva 07ade4c822
feat: Expose _private names 2023-12-04 23:36:09 -08:00
Leni Aniva a454aaf1d4
feat: Remove stem deduce 
Some private subproofs are not shown in the catalog and this breaks
dependencies
 2023-12-04 16:40:15 -08:00
Leni Aniva ec09304e02
feat: Remove printing projections 2023-12-04 16:21:02 -08:00
Leni Aniva 967e3dfb4f
feat: Remove | in symbol output 2023-11-27 09:54:41 -08:00
Leni Aniva 0a5a96275f
chore: Version bump to 0.2.9 2023-11-26 23:48:47 -08:00
Leni Aniva 7690272bfa
feat: Shorter symbol category 2023-11-26 22:14:58 -08:00
Leni Aniva 7b59937853
feat: Read dependencies of library symbols 2023-11-25 15:07:56 -08:00
Leni Aniva 2a9931c134
fix: Rectify error format 2023-11-09 22:24:17 -08:00
Leni Aniva c99125c4a6 Merge pull request 'feat: Allow selective continuation of goals' (#27) from goal/continuation into dev 
Reviewed-on: #27
 2023-11-07 16:49:55 -08:00
Leni Aniva 8218d3f004
fix: Do not show parent state in continue 2023-11-07 13:10:14 -08:00
Leni Aniva 736e68639f
fix: New goal state not inserted correctly 2023-11-07 13:07:50 -08:00
Leni Aniva cfd1cfd107
Merge branch 'dev' into goal/continuation 2023-11-07 12:11:14 -08:00
Leni Aniva 764be6d14b
fix: Remove the error prone SemihashMap 2023-11-07 12:09:54 -08:00