Library gaia_hydras.HydraGaia_Examples
From mathcomp Require Import all_ssreflect zify.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic.
From hydras Require Import T1 E0 Hessenberg.
From gaia Require Export ssete9.
From gaia_hydras Require Import T1Bridge GCanon GHessenberg
GLarge_Sets.
Set Implicit Arguments.
Check \F 42.
Example α : T1 :=
T1omega + phi0 T1omega × \F 3 + phi0 (\F 5) × \F 4 + T1omega × T1omega.
Example β : T1 := phi0 (phi0 (\F 2)).
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic.
From hydras Require Import T1 E0 Hessenberg.
From gaia Require Export ssete9.
From gaia_hydras Require Import T1Bridge GCanon GHessenberg
GLarge_Sets.
Set Implicit Arguments.
Check \F 42.
Example α : T1 :=
T1omega + phi0 T1omega × \F 3 + phi0 (\F 5) × \F 4 + T1omega × T1omega.
Example β : T1 := phi0 (phi0 (\F 2)).
Hessenberg's sum
Print oplus.
Check T1lt (\F 42) T1omega.
Check (\F 42 < T1omega)%ca.
Check \F 42 < T1omega.
Check T1.lt (T1.T1nat 42) T1.T1omega.
Check T1.lt (\F 42)%t1 T1.T1omega.