Agda, ключевое слово `with` и` refl` [duplicate]

Question

Agda, ключевое слово `with` и` refl` [duplicate]

Попробуйте этот метод. Он должен работать, когда поле, когда вы хотите сохранить изображение, имеет тип bytea. Сначала он создает byte[] для изображения. Затем он сохраняет его с помощью IDataParameter типа binary.

    public static void PerisitImage(string path, IDbConnection connection)
    {
        using (var command = connection.CreateCommand ())
        {
            Image img = Image.FromFile (path);
            MemoryStream tmpStream = new MemoryStream();
            img.Save (tmpStream, ImageFormat.Png); // change to other format
            tmpStream.Seek (0, SeekOrigin.Begin);
            byte[] imgBytes = new byte[MAX_IMG_SIZE];
            tmpStream.Read (imgBytes, 0, MAX_IMG_SIZE);

            command.CommandText = "INSERT INTO images(payload) VALUES (:payload)";
            IDataParameter par = command.CreateParameter();
            par.ParameterName = "payload";
            par.DbType = DbType.Binary;
            par.Value = imgBytes;
            command.Parameters.Add(par);
            command.ExecuteNonQuery ();
        }
    }

3

agda

задан nicolas 27 December 2014 в 13:45

1 ответ

Другие вопросы по тегам:

agda

Похожие вопросы:

score 3 · Accepted Answer

Просто не совпадайте с шаблоном на p x:

predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {x :: xs} with inspect (p x) 
predicate {A} {p} {x :: xs} | it true  pf rewrite pf = {!!}
predicate {A} {p} {x :: xs} | it false pf rewrite pf = {!!}

Обратите внимание, что идиома inspect устарела. Используйте для проверки стероидов . Вы можете найти его в стандартной библиотеке здесь .

Ваш код становится

predicate : ∀ {A : Set} {p : A -> Bool } {xs : List A } -> 
            All (satisfies p) (filter p xs)  
predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {xs = x :: xs} with p x | inspect p x
predicate {A} {p} {x :: xs} | true  | [ pf ] = {!!}
predicate {A} {p} {x :: xs} | false | [ pf ] = {!!}

, когда pf находится в первом отверстии

.Data.Unit.Core.reveal (.Data.Unit.Core.hide p x) == true

, который бета-уменьшается до p x == true. То есть если у вас есть

test : ∀ {A : Set} {p : A -> Bool} {x} -> p x == true -> True
test _ = _

, тогда размещение test {p = p} pf в первом отверстии и ввод C-c C-d дает вам True.

3

ответ дан user3237465 17 August 2018 в 11:51

1

ах. почему я сам не думал об этом :) Спасибо за руководство, я думаю, мне придется подробно рассмотреть его сегодня днем. – nicolas 27 December 2014 в 14:37
2

довольно потрясающе. Я не уверен, что действительно по-настоящему понимаю большую картину механизма игры в Inspect on steroid. замечание «Легко показать, что раскрытие x дает вам раскрыть x: & quot; выделите, что возврат ограничен определенным типом, который, как я полагаю, имеет решающее значение. – nicolas 27 December 2014 в 16:03
3

здесь многое можно понять. Кажется, я понял, но это было не тривиально для меня ... – nicolas 27 December 2014 в 18:19
4

@nicolas, если вы говорите о последнем редактировании, которое я сделал, я удалил его, так как я не уверен, если это имеет смысл. Я верну его, после того, как убедился. Простите за это. – user3237465 27 December 2014 в 18:37
5

Раньше я не видел удаленное редактирование, это кажется замечательным, но даже ответ, поскольку он предоставляет очень полезные ссылки на разные стратегии: переписать VS на стероид. тем более полезным, что это не в AgdaIntro pdf. Вы активно используете Agda? – nicolas 27 December 2014 в 20:23