1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
//! Logical type implication.
/// Enables implication from a source refinement into a target refinement when the source can be guaranteed
/// to satisfy the predicate of the target.
///
/// For example, if we have a `Refinement<u8, LessThan<100>>`, then we can be sure that the value contained
/// within the refinement is less than 100. This also logically implies that the value is less than 101,
/// 105, or indeed any value greater than 100.
///
/// With the `implication` feature enabled (and the corresponding language feature enabled, `generic_const_exprs`),
/// `Implies` allows us to encode this relationship like so:
///
/// ```
/// #![allow(incomplete_features)]
/// #![feature(generic_const_exprs)]
///
/// use refined::{Refinement, RefinementOps, boundable::unsigned::LessThan, Implies};
///
/// fn takes_lt_100(value: Refinement<u8, LessThan<100>>) -> String {
/// format!("{}", value)
/// }
///
/// let lt_50: Refinement<u8, LessThan<50>> = Refinement::refine(49).unwrap();
/// let ex: Refinement<u8, LessThan<51>> = lt_50.imply();
/// let result = takes_lt_100(lt_50.imply());
/// assert_eq!(result, "49");
/// ```
///
/// ## Implementation
///
/// While it is possible to create your own `Implies` implementations, doing so will require some type-level
/// machinery that isn't exposed by `std`, and that `refined` also keeps private. Because `generic_const_exprs`
/// is unstable, there is a good chance that the implementation details behind `implication` may change
/// significantly in the future, and I do not wish this these changes to require a major version release.
///
/// See [the source](https://github.com/jkaye2012/refined/blob/main/src/implication/boundable_imp.rs#L5-L18)
/// for an example of how the internals work currently. To create your own implementation, you need some version
/// of `Assert` and `IsTrue`. The idea is that the generic const expr in the `Implies` implementation trait
/// bound will only resolve to a valid `IsTrue` implementation when the logical predicate is satisfied.
pub
pub
pub use *;