Skip to content

Commit

Permalink
Add test snapshot for constructor-as-closure.
Browse files Browse the repository at this point in the history
  • Loading branch information
maximebuyse committed Oct 24, 2024
1 parent 5bc769e commit f3c9824
Showing 1 changed file with 46 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
---
source: test-harness/src/harness.rs
expression: snapshot
info:
kind:
Translate:
backend: fstar
info:
name: constructor-as-closure
manifest: constructor-as-closure/Cargo.toml
description: ~
spec:
optional: false
broken: false
issue_id: ~
positive: true
snapshot:
stderr: false
stdout: true
include_flag: ~
backend_options: ~
---
exit = 0

[stdout]
diagnostics = []

[stdout.files]
"Constructor_as_closure.fst" = '''
module Constructor_as_closure
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

type t_Context =
| Context_A : i32 -> t_Context
| Context_B : i32 -> t_Context

type t_Test = | Test : i32 -> t_Test

let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test =
Core.Option.impl__map #i32 #t_Test x Test

let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
Core.Option.impl__map #i32 #t_Context x Context_B
'''

0 comments on commit f3c9824

Please sign in to comment.