blob: 37f0dffbdcaaa20f94d7933a1b12a62a516e8c0a (
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
namespace polonius_list
/- [polonius_list::List]
Source: 'src/polonius_list.rs', lines 3:0-3:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [polonius_list::get_list_at_x]: forward function
Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
match ls with
| List.Cons hd tl =>
if hd = x
then Result.ret (List.Cons hd tl)
else get_list_at_x tl x
| List.Nil => Result.ret List.Nil
/- [polonius_list::get_list_at_x]: backward function 0
Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x_back
(ls : List U32) (x : U32) (ret : List U32) : Result (List U32) :=
match ls with
| List.Cons hd tl =>
if hd = x
then Result.ret ret
else
do
let tl0 ← get_list_at_x_back tl x ret
Result.ret (List.Cons hd tl0)
| List.Nil => Result.ret ret
end polonius_list
|
