Skip to content
This repository has been archived by the owner on Sep 5, 2022. It is now read-only.

bind many name with type #20

Closed
4 tasks done
dannypsnl opened this issue Aug 24, 2021 · 0 comments · Fixed by #27
Closed
4 tasks done

bind many name with type #20

dannypsnl opened this issue Aug 24, 2021 · 0 comments · Fixed by #27
Assignees
@CYBAI
Labels
enhancement More like an internal feature, improve code base but not surface feature New feature or request
Projects
simple theorem prover

Comments

@dannypsnl
Copy link
Owner

dannypsnl commented Aug 24, 2021 •
edited
Loading

The current bind is like

(def (foo [x : A] [y : A]) : A
  [x => y])

would be good to have

(def (foo [x y : A]) : A
  [x => y])
  • extract bindings
  • update data type bindings
  • update data type constructor bindings
  • update def bindings
@dannypsnl dannypsnl added enhancement More like an internal feature, improve code base but not surface feature New feature or request labels Aug 24, 2021
@dannypsnl dannypsnl moved this from To do to In progress in simple theorem prover Aug 25, 2021
dannypsnl added a commit that referenced this issue Aug 26, 2021
@dannypsnl
dev(extract bind)
01a7387 
ref #20
dannypsnl added a commit that referenced this issue Aug 26, 2021
@dannypsnl
form(extract bindings)
0eb40d5 
ref #20
CYBAI added a commit that referenced this issue Aug 29, 2021
@CYBAI
bind(share type)
d495242 
Implement share type bindings.

Resolve #20
@CYBAI CYBAI mentioned this issue Aug 29, 2021
Merged
simple theorem prover automation moved this from In progress to Done Aug 29, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@CYBAI CYBAI

Labels
enhancement More like an internal feature, improve code base but not surface feature New feature or request
Projects
No open projects
simple theorem prover
  
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

bind(share type) dannypsnl/k
2 participants
@CYBAI @dannypsnl