Created
July 4, 2018 10:06
-
-
Save petermarks/f8802cc66549226125e4b6a8fee373c5 to your computer and use it in GitHub Desktop.
Proving record field get and set are an identity for the field value
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| record R where | |
| constructor MkR | |
| foo : Nat | |
| foo_identity : (foo (set_foo x r)) = x | |
| foo_identity {x} {r} with (foo (set_foo x r)) | |
| foo_identity {x} | y = ?rhs |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment