refactor: use expressiveness-from-compiler when applicable

ibbem · ibbem · commit ef1733d2cf4d · 2025-07-03T19:10:30.000+02:00
diff --git a/src/Vatras/Translation/Lang/VariantList-to-VT.agda b/src/Vatras/Translation/Lang/VariantList-to-VT.agda
@@ -184,7 +184,7 @@ VariantList→VT = record
   }
 
 VT≽VariantList : VTL ≽ VariantListL
-VT≽VariantList {A} e = translate e , ≅[]→≅ (LanguageCompiler.preserves VariantList→VT e)
+VT≽VariantList = expressiveness-from-compiler VariantList→VT
 
 VT-is-complete : Complete VTL
 VT-is-complete = completeness-by-expressiveness (VariantList-is-Complete) VT≽VariantList

Original file line number	Diff line number	Diff line change
`@@ -184,7 +184,7 @@ VariantList→VT = record`
`184`	`184`	`}`
`185`	`185`
`186`	`186`	`VT≽VariantList : VTL ≽ VariantListL`
`187`		`-VT≽VariantList {A} e = translate e , ≅[]→≅ (LanguageCompiler.preserves VariantList→VT e)`
	`187`	`+VT≽VariantList = expressiveness-from-compiler VariantList→VT`
`188`	`188`
`189`	`189`	`VT-is-complete : Complete VTL`
`190`	`190`	`VT-is-complete = completeness-by-expressiveness (VariantList-is-Complete) VT≽VariantList`