Commit 4667eb8f authored by Martin PORTALIER's avatar Martin PORTALIER

Update fixedpoint_lemmas.v

parent 129ace72
Pipeline #19279 failed with stages
in 1 minute and 52 seconds
Require Import rt.util.tactics. Require Import rt.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Martin : I didn't use this file, it can be deleted. *)
Section FixedPoint. Section FixedPoint.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment