package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file simple_check.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
let simple_check1 env sigma evalue =
(* This version should be preferred if you want to really
  verify that the input is well-typed,
  and if you want to obtain the type. *)
(* Note that the output value is a pair containing a new evar_map:
   typing will fill out blanks in the term by add evar bindings. *)
  Typing.type_of env sigma evalue

let simple_check2 env sigma evalue =
(* This version should be preferred if you already expect the input to
  have been type-checked before.  Set ~lax to false if you want an anomaly
  to be raised in case of a type error.  Otherwise a ReTypeError exception
  is raised. *)
  Retyping.get_type_of ~lax:true env sigma evalue
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct