(match typ with None -> "?" | Some typ -> pp_term typ)
(pp_term ~pp_parens:true body)
| Ast.Binder (kind, var, body) ->
(match typ with None -> "?" | Some typ -> pp_term typ)
(pp_term ~pp_parens:true body)
| Ast.Binder (kind, var, body) ->
(pp_term ~pp_parens:true body)
| Ast.Case (term, indtype, typ, patterns) ->
sprintf "match %s%s%s with %s"
(pp_term ~pp_parens:true body)
| Ast.Case (term, indtype, typ, patterns) ->
sprintf "match %s%s%s with %s"
(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
| Ast.LetIn (var, t1, t2) ->
(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
| Ast.LetIn (var, t1, t2) ->
(pp_term ~pp_parens:true t2)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
(pp_term ~pp_parens:true t2)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
and pp_box_spec (kind, spacing, indent) =
let int_of_bool b = if b then 1 else 0 in
let kind_string =
and pp_box_spec (kind, spacing, indent) =
let int_of_bool b = if b then 1 else 0 in
let kind_string =
| Ast.Inductive (params, types) ->
let pp_constructors constructors =
String.concat "\n"
| Ast.Inductive (params, types) ->
let pp_constructors constructors =
String.concat "\n"
| (name, inductive, typ, constructors) :: tl ->
let fst_typ_pp =
sprintf "%sinductive %s%s: %s \\def\n%s"
| (name, inductive, typ, constructors) :: tl ->
let fst_typ_pp =
sprintf "%sinductive %s%s: %s \\def\n%s"
| Ast.Theorem (flavour, name, typ, body) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)
| Ast.Theorem (flavour, name, typ, body) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)
| None -> ""
| Some body -> "\\def\n " ^ pp_term body)
| Ast.Record (params,name,ty,fields) ->
| None -> ""
| Some body -> "\\def\n " ^ pp_term body)
| Ast.Record (params,name,ty,fields) ->
- "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^
- " \\def {" ^ pp_fields fields ^ "\n}"
+ "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^
+ " \\def {" ^ pp_fields pp_term fields ^ "\n}"