blob: 489871ba1bd8b58fb59fc0b3e7ded216aad6b8d9 (
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
28
29
30
31
32
33
34
35
36
37
38
|
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [polonius_list]
import Base
open Primitives
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false
namespace polonius_list
/- [polonius_list::List]
Source: 'tests/src/polonius_list.rs', lines 6:0-6:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [polonius_list::get_list_at_x]:
Source: 'tests/src/polonius_list.rs', lines 16:0-16:76 -/
divergent def get_list_at_x
(ls : List U32) (x : U32) :
Result ((List U32) × (List U32 → Result (List U32)))
:=
match ls with
| List.Cons hd tl =>
if hd = x
then Result.ok (List.Cons hd tl, Result.ok)
else
do
let (l, get_list_at_x_back) ← get_list_at_x tl x
let back :=
fun ret =>
do
let tl1 ← get_list_at_x_back ret
Result.ok (List.Cons hd tl1)
Result.ok (l, back)
| List.Nil => Result.ok (List.Nil, Result.ok)
end polonius_list
|
