Alex Rozanov hacklex
This file contains hidden or 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
| module Bug | |
| type binary_op (a:Type) = a -> a -> a | |
| type unary_op (a:Type) = a -> a | |
| type predicate (a:Type) = a -> bool | |
| type binary_relation (a: Type) = a -> a -> bool | |
| [@@"opaque_to_smt"] | |
| let is_reflexive (#a:Type) (r: binary_relation a) = forall (x:a). x `r` x | |
| [@@"opaque_to_smt"] |
This file contains hidden or 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
| scopeName: 'source.fstar' | |
| name: 'F*' | |
| fileTypes: [ 'fst', 'fsti', 'fs7' ] | |
| patterns: [ | |
| { include: '#comments' } | |
| { include: '#modules' } | |
| { include: '#options' } |
hacklex
/ AlgebraTypes.fst
Last active
July 23, 2021 22:18
line 285 admit is redundant, but F* fails without it!
This file contains hidden or 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
| module AlgebraTypes | |
| #push-options "--ifuel 0 --fuel 0 --z3rlimit 1" | |
| type binary_op (a:Type) = a -> a -> a | |
| type unary_op (a:Type) = a -> a | |
| type predicate (a:Type) = a -> bool | |
| type binary_relation (a: Type) = a -> a -> bool | |
| let is_reflexive (#a:Type) (r: binary_relation a) = forall (x:a). x `r` x |
NewerOlder