File: factory_when_notation.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 (7 lines) | stat: -rw-r--r-- 219 bytes parent folder | download 
1
2
3
4
5
6
7
 
From HB Require Import structures.
Notation x := (fun x : nat => true).
HB.mixin Record m T := {x : T}.
HB.factory Record f T := { x : T }.
HB.builders Context T of f T.
HB.instance Definition _ := m.Build T x.
HB.end.