blob: bec63e60a99c0d9995af145127d8dc1a475c813c (
plain)
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
|
inductive V₃ where
| true : V₃
| false : V₃
| indeterminate : V₃
inductive V₆ where
| true_deny : V₆
| true_permit : V₆
| indeterminate_deny : V₆
| indeterminate_permit : V₆
| indeterminate : V₆
| false : V₆
inductive Decision where
| permit : Decision
| deny : Decision
deriving Repr
-- structure Result where
-- decision : Decision
-- obligations : Option (List String)
-- advice : Option (List String)
-- deriving Repr
def Result (α : Type) : Type := Decision × α
#check ((Decision.permit, "Hi!") : Result String)
|
© 2015 - 2026 Jakob L. Kreuze
