Skip to content

Commit

Permalink
formating
Browse files Browse the repository at this point in the history
  • Loading branch information
lfrenot committed Jan 17, 2025
1 parent 895353f commit 573e520
Showing 1 changed file with 14 additions and 14 deletions.
28 changes: 14 additions & 14 deletions src/sail_lean_backend/pretty_print_lean.ml
Original file line number Diff line number Diff line change
Expand Up @@ -380,20 +380,20 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
| E_app (Id_aux (Id "internal_pick", _), _) ->
string "sorry" (* TODO replace by actual implementation of internal_pick *)
| E_internal_plet (pat, e1, e2) ->
(* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *)
let e0 = doc_pat ctxt false pat in
let e1_pp = doc_exp ctxt e1 in
let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in
let e2_pp = doc_exp ctxt e2' in
(* infix 0 1 middle e1_pp e2_pp *)
let e0_pp =
begin
match pat with
| P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ""
| _ -> separate space [string "let"; e0; string ":="] ^^ space
end
in
e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp
(* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *)
let e0 = doc_pat ctxt false pat in
let e1_pp = doc_exp ctxt e1 in
let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in
let e2_pp = doc_exp ctxt e2' in
(* infix 0 1 middle e1_pp e2_pp *)
let e0_pp =
begin
match pat with
| P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ""
| _ -> separate space [string "let"; e0; string ":="] ^^ space
end
in
e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp
| E_app (f, args) ->
let d_id =
if Env.is_extern f env "lean" then string (Env.get_extern f env "lean")
Expand Down

0 comments on commit 573e520

Please sign in to comment.