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

check body of def function #16

Closed
dannypsnl opened this issue Aug 21, 2021 · 1 comment
Closed

check body of def function #16

dannypsnl opened this issue Aug 21, 2021 · 1 comment
Assignees
Labels
bug Something isn't working

Comments

@dannypsnl
Copy link
Owner

dannypsnl commented Aug 21, 2021

The following code shouldn't work but pass our type checking:

(def (foo [x : Nat]) : Bool
  [x => x])

This is because we didn't check the function body correctly.

NOTE: Worth taking a look into https://github.com/yjqww6/macrology/blob/master/intdef-ctx.md

@dannypsnl dannypsnl added the bug Something isn't working label Aug 21, 2021
@dannypsnl dannypsnl self-assigned this Aug 21, 2021
@dannypsnl dannypsnl pinned this issue Aug 21, 2021
@dannypsnl

This comment has been minimized.

@dannypsnl dannypsnl unpinned this issue Aug 25, 2021
@dannypsnl dannypsnl added this to In progress in simple theorem prover Aug 25, 2021
simple theorem prover automation moved this from In progress to Done Mar 30, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

2 participants