aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

feat: Prograde tactics #83

Merged
aniva merged 24 commits from tactic/eval into dev 2024-08-31 20:04:39 -07:00
Conversation 1 Commits 24 Files Changed 25 +872 -739

24 Commits

Author SHA1 Message Date
Leni Aniva edec0f5733
feat: Use CoreM for diag monad 2024-08-26 13:42:14 -04:00
Leni Aniva 0c529c5cd9
Merge branch 'misc/test-driver' into tactic/eval 2024-08-18 12:24:26 -07:00
Leni Aniva 3733c10a4e
refactor: Unify call convention 
Induction like tactics should return `Array InductionSubgoal`. Branching
tactics should return their branch first.
 2024-08-17 16:47:21 -07:00
Leni Aniva 5d43068ec3
fix: Flake check failure 2024-08-17 02:07:17 -07:00
Leni Aniva f87eed817f
build: Move non-package output to legacyPackages 2024-08-17 01:59:48 -07:00
Leni Aniva 43e11f1ba3
refactor: Always display isInaccessible 2024-08-17 00:53:38 -07:00
Leni Aniva 0c469027c6
fix: Refactor mvar collection in assign tactic 2024-08-17 00:50:02 -07:00
Leni Aniva e1b7eaab12
fix: Let tactic not bringing binder into scope 2024-08-17 00:47:12 -07:00
Leni Aniva d17b21e282
fix: Use `getMVarsNoDelayed` 2024-08-16 00:32:34 -07:00
Leni Aniva 5b4f8a37eb
refactor: All Tactic/ tactics into MetaM form 2024-08-15 23:41:17 -07:00
Leni Aniva 1e7a186bb1
refactor: MetaM form of define (evaluate) 2024-08-15 23:23:17 -07:00
Leni Aniva 9b0456a5e0
refactor: MetaM form of have and let 2024-08-15 23:17:15 -07:00
Leni Aniva 7968072097
refactor: Remove the newMVarSet mechanism 
This field has ambiguous purpose and does not account for different
types of mvars
 2024-08-15 22:53:42 -07:00
Leni Aniva e07f9d9b3f
Merge branch 'dev' into tactic/eval 2024-08-15 22:45:43 -07:00
Leni Aniva df8b6602ee
Merge branch 'misc/version' into tactic/eval 2024-07-06 20:00:12 -07:00
Leni Aniva 4549ae1f65
Merge branch 'misc/version' into tactic/eval 2024-07-06 19:56:31 -07:00
Leni Aniva 6ddde2963d
test: Eval instantiate 2024-06-27 14:51:16 -04:00
Leni Aniva fc0d872343
refactor: Simplify proof test infrastructure 2024-06-27 14:34:21 -04:00
Leni Aniva 2d2ff24017
feat: FFI interface for `evaluate` tactic 2024-06-25 17:10:31 -04:00
Leni Aniva 7acf1ffdf1
refactor: Move `have` to prograde tactic 2024-06-25 16:58:35 -04:00
Leni Aniva 58f9d72288
test: Evaluate tactic context 2024-06-25 16:18:31 -04:00
Leni Aniva c0124b347f
Merge branch 'serial/expr' into tactic/eval 2024-06-25 16:05:20 -04:00
Leni Aniva e282d9f781
test: Evaluation tactic 2024-06-25 11:03:08 -04:00
Leni Aniva 25a7025c25
feat: Evaluation tactic 2024-06-23 15:01:51 -07:00