File: structures.v

package info (click to toggle)
coq-hierarchy-builder 1.8.1-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,988 kB
  • sloc: makefile: 109
file content (11 lines) | stat: -rw-r--r-- 452 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
 
From Coq Require Import String ssreflect ssrfun.
Export String.StringSyntax.

Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
  phantom T1 t1 -> phantom T2 t2.
Definition id_phant {T} {t : T} (x : phantom T t) := x.
Definition nomsg : error_msg := NoMsg.
Definition is_not_canonically_a x := IsNotCanonicallyA x.
Definition new {T} (x : T) := x.
Definition eta {T} (x : T) := x.