meta.yml

---
fullname: FlocqLecture
shortname: FlocqLecture
organization: thery
community: false
dune: false
action: true

synopsis: Lectures about flocq

description: |-
  This is an introductory course **Floating-Point Numbers and Formal Proof**
  given at [ENS Lyon](https://www.ens-lyon.fr/LIP/) in 2016-2017.
  It is based on the [Flocq Library](https://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 (Laurent.Thery@inria.fr)

authors:
- name: Laurent Théry

maintainers:
- name: Laurent Théry
  nickname: thery

opam-file-maintainer: thery@sophia.inria.fr

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: '8.16 or later'
  opam: '{(>= "8.16")}'

dependencies:
- opam:
    name: coq-flocq
    version: '{(>= "4.1.0")}'
  description: |-
    [Flocq 4.1 or later](https://gitlab.inria.fr/flocq/flocq.git)

tested_coq_opam_versions:
- version: '8.16'

namespace: FlocqLecture

keywords:
- name: Flocq Lecture
- name: Flocq tutorial


---