0xameer
- https://keyoxide.org/jasitis@gmail.com
- https://github.com/tailgitfp
0xameer
/ modal_mu.v
Created
May 11, 2023 18:23
— forked from qnighy/modal_mu.v
Modal mu calculus in Coq
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Classes.SetoidClass. | |
| Program Instance Iff1Setoid{A:Type} : Setoid (A->Prop) := {| | |
| equiv := fun P Q => forall x, P x <-> Q x | |
| |}. | |
| Next Obligation. | |
| split. | |
| - intros P x; reflexivity. | |
| - intros P Q H x; symmetry; exact (H x). | |
| - intros P Q R H0 H1 x; transitivity (Q x); [exact (H0 x)|exact (H1 x)]. |
0xameer
/ LICENSE.txt
Created
September 28, 2011 19:21
— forked from p01/LICENSE.txt
Sudoku Solver in 140bytes
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| DO WHAT THE FUCK YOU WANT TO PUBLIC LICENSE | |
| Version 2, December 2004 | |
| Copyright (C) 2011 Mathieu 'p01' Henri <http://www.p01.org/releases/> | |
| Everyone is permitted to copy and distribute verbatim or modified | |
| copies of this license document, and changing it is allowed as long | |
| as the name is changed. | |
| DO WHAT THE FUCK YOU WANT TO PUBLIC LICENSE |
NewerOlder