# This file was generated from `meta.yml`, please do not edit manually.

# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"

maintainer: "[email protected]"

version: "dev"

homepage: "https://github.com/thery/FlocqLecture"

dev-repo: "git https://github.com/thery/FlocqLecture.git"

bug-reports: "https://github.com/thery/FlocqLecture/issues"

license: "MIT"

synopsis: "Lectures about flocq"

description: """

This is an introductory course **Floating-Point Numbers and Formal Proof**

given at [ENS Lyon](http://www.ens-lyon.fr/LIP/) in 2016-2017.

It is based on the [Flocq Library](http://flocq.gforge.inria.fr/).

----

It is composed of four lectures:

1. [Real numbers](./lecture1.v) ([solution](./lecture1_solution.v))

2. [Rounding](./lecture2.v) ([solution](./lecture2_solution.v))

3. [Proof I](./lecture3.v) ([solution](./lecture3_solution.v))

4. [Proof II](./lecture3.v) ([solution](./lecture4_solution.v))

----

Laurent Théry ([email protected])"""

build: [make "-j%{jobs}%"]

install: [make "install"]

depends: [

"coq" {(>= "8.16")}

"coq-flocq" {(>= "4.1.0")}

]

tags: [

"keyword:Flocq Lecture"

"keyword:Flocq tutorial"

"logpath:FlocqLecture"

]

authors: [

"Laurent Théry"

]